From af2c82cfd7f2318fcd81da2ea4cf3fd695db3b40 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Wed, 28 Apr 2021 18:14:53 +0200
Subject: start the new "BTL" IR.

---
 lib/OptionMonad.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'lib/OptionMonad.v')

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.
-- 
cgit