From e04692c31b3e6edceaa8c97e7c7f343feb8b56c0 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Wed, 5 May 2021 11:49:05 +0100 Subject: Solve iter_expand_instr_spec by tactic (not Icall) --- src/common/Vericertlib.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/common') diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index 6437612..1c5c37f 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -57,9 +57,10 @@ 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_apply H := +Ltac auto_apply fact := + let H' := fresh "H" in match goal with - | H' : _ |- _ => apply H in H' + | H : _ |- _ => pose proof H as H'; apply fact in H' end. (** Specialize all hypotheses with a forall to a specific term *) -- cgit