From 564fb33a504d7611d73bbe5e20b23453e141ed3d Mon Sep 17 00:00:00 2001
From: Michalis Pardalos <m.pardalos@gmail.com>
Date: Sun, 2 May 2021 11:12:45 +0100
Subject: Simplify some HTLgenspec proofs

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

(limited to 'src/common')

diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index c537cef..722edef 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -57,6 +57,11 @@ Ltac learn_tac fact name :=
 Tactic Notation "learn" constr(fact) := let name := fresh "H" in learn_tac fact name.
 Tactic Notation "learn" constr(fact) "as" simple_intropattern(name) := learn_tac fact name.
 
+Ltac auto_hyp H :=
+  match goal with
+  | H' : _ |- _ => solve [ apply H in H'; auto | auto ]
+  end.
+
 Ltac unfold_rec c := unfold c; fold c.
 
 Ltac solve_by_inverts n :=
-- 
cgit