From 35487b45f778b15118d3cc934622b35429a4c899 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Tue, 11 May 2021 16:02:08 +0200
Subject: better autodestruct ?

---
 lib/OptionMonad.v         | 17 ++++++++++++++++-
 scheduling/BTL_SEtheory.v | 16 ----------------
 2 files changed, 16 insertions(+), 17 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
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;
-- 
cgit