aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/RTLpathSE_simu_specs.v
diff options
context:
space:
mode:
Diffstat (limited to 'scheduling/RTLpathSE_simu_specs.v')
-rw-r--r--scheduling/RTLpathSE_simu_specs.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v
index c6a4d409..c3266db9 100644
--- a/scheduling/RTLpathSE_simu_specs.v
+++ b/scheduling/RTLpathSE_simu_specs.v
@@ -309,7 +309,6 @@ End HFINAL_REFINES.
Section FAKE_HSVAL.
(* BEGIN "fake" hsval without real hash-consing *)
(* TODO:
- 1) put these definitions elsewhere ? in RTLpathSE_simu_specs.v ?
2) reuse these definitions in hSinput, hSop, etc
in order to factorize proofs ?
*)