diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-04-28 18:14:53 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-04-28 18:14:53 +0200 |
| commit | af2c82cfd7f2318fcd81da2ea4cf3fd695db3b40 (patch) | |
| tree | 7a5f98548a3e3e0497231627166738253cbce506 /lib/OptionMonad.v | |
| parent | 71d69df10047aa5710adb4bcdc75e18bec4dbf27 (diff) | |
| download | compcert-kvx-af2c82cfd7f2318fcd81da2ea4cf3fd695db3b40.tar.gz compcert-kvx-af2c82cfd7f2318fcd81da2ea4cf3fd695db3b40.zip | |
start the new "BTL" IR.
Diffstat (limited to 'lib/OptionMonad.v')
| -rw-r--r-- | lib/OptionMonad.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/lib/OptionMonad.v b/lib/OptionMonad.v index 824a9c2f..d2563c97 100644 --- a/lib/OptionMonad.v +++ b/lib/OptionMonad.v @@ -13,6 +13,12 @@ Local Open Scope option_monad_scope. (** Simple tactics for option-monad *) +Ltac 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 + end. + Lemma destruct_SOME A B (P: option B -> Prop) (e: option A) (f: A -> option B): (forall x, e = Some x -> P (f x)) -> (e = None -> P None) -> (P (SOME x <- e IN f x)). Proof. |