diff options
Diffstat (limited to 'scheduling/BTL_SEtheory.v')
-rw-r--r-- | scheduling/BTL_SEtheory.v | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 5f7ecb1b..b9a05a8a 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -13,22 +13,6 @@ Require Import RTL BTL OptionMonad. Ltac inversion_SOME := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) - -Ltac depmatch exp := - match exp with - | context f [match ?expr with | _ => _ end] => ltac: (depmatch expr) - | _ => exp - end. - -Ltac autodestruct := - let EQ := fresh "EQ" in - match goal with - | |- context f [match ?expr with | _ => _ end] => - let t := ltac: (depmatch expr) in - destruct t eqn:EQ; generalize EQ; clear EQ; congruence || trivial - end. - - Record iblock_exec_context := Bctx { cge: BTL.genv; cstk: list stackframe; |