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 /lib | |
parent | 473c17f114f44756c3803c026266417dfe92c242 (diff) | |
download | compcert-kvx-35487b45f778b15118d3cc934622b35429a4c899.tar.gz compcert-kvx-35487b45f778b15118d3cc934622b35429a4c899.zip |
better autodestruct ?
Diffstat (limited to 'lib')
-rw-r--r-- | lib/OptionMonad.v | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/lib/OptionMonad.v b/lib/OptionMonad.v index d2563c97..18430e04 100644 --- a/lib/OptionMonad.v +++ b/lib/OptionMonad.v @@ -13,7 +13,22 @@ Local Open Scope option_monad_scope. (** Simple tactics for option-monad *) -Ltac autodestruct := +Ltac deepest_match exp := + match exp with + | context f [match ?expr with | _ => _ end] => ltac: (deepest_match expr) + | _ => exp + end. + +Ltac autodestruct := + let EQ := fresh "EQ" in + match goal with + | |- context f [match ?expr with | _ => _ end] => + let t := ltac: (deepest_match expr) in + destruct t eqn:EQ; generalize EQ; clear EQ; congruence || trivial + end. + +(* deprecated version of "autodestruct". the new one seems a better replacement *) +Ltac dummy_autodestruct := let EQ := fresh "EQ" in match goal with | |- context f [match ?expr with | _ => _ end] => destruct expr eqn:EQ; generalize EQ; clear EQ; congruence || trivial |