Changeset 2288 for src/RTLabs/CostSpec.ma

Timestamp:

Aug 2, 2012, 5:04:36 PM (8 years ago)

Author:

campbell

Message:

Remove jumptables from RTLabs. :(

File:

• src/RTLabs/CostSpec.ma (modified) (2 diffs)

src/RTLabs/CostSpec.ma

@@ -22 +22 @@
     is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
     is_cost_label (lookup_present … (f_graph f) l2 ?) = true
-| St_jumptable _ ls ⇒ λH.
+(*| St_jumptable _ ls ⇒ λH.
     (* I did have a dependent version of All here, but it's a pain. *)
-    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
+    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls*)
 | _ ⇒ λ_. True
 ]. whd in H;
@@ -55 +55 @@
 *)
 | St_cond _ l1 l2 ⇒ [l1; l2]
-| St_jumptable _ ls ⇒ ls
+(*| St_jumptable _ ls ⇒ ls*)
 | St_return ⇒ [ ]
 ].