From 5e17f4a83b3fe5b8fdf58ab9643e33543d257bad Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 5 Nov 2023 10:32:47 +0100
Subject: Finish load proof

---
 src/common/Vericertlib.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/common/Vericertlib.v')

diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index da046f3..0310c19 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -82,6 +82,12 @@ Ltac destruct_match :=
 
 Ltac auto_destruct x := destruct x eqn:?; simpl in *; try discriminate; try congruence.
 
+  Ltac destin x := 
+    match type of x with 
+    | context[match ?y with _ => _ end] => let DIN := fresh "DIN" in destruct y eqn:DIN
+    | _ => fail
+    end.
+
 Ltac nicify_hypotheses :=
   repeat match goal with
          | [ H : ex _ |- _ ] => inv H
-- 
cgit