diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-11 16:02:08 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-11 16:02:08 +0200 |
| commit | 35487b45f778b15118d3cc934622b35429a4c899 (patch) | |
| tree | 21a2210c039f22640c33c1b65c28c10975dd8818 /scheduling/BTL_SEtheory.v | |
| parent | 473c17f114f44756c3803c026266417dfe92c242 (diff) | |
| download | compcert-kvx-35487b45f778b15118d3cc934622b35429a4c899.tar.gz compcert-kvx-35487b45f778b15118d3cc934622b35429a4c899.zip | |
better autodestruct ?
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; |