From 30e4a8375f973840bf4faf7cf1f37340fbb20979 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 10 Oct 2016 17:19:06 -0400 Subject: specialize_by: explicitly maintain transparency --- src/Util/Tactics.v | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'src/Util/Tactics.v') diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 502e79332..69e74a3fe 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -252,11 +252,20 @@ Ltac destruct_sig_matcher HT := Ltac destruct_sig := destruct_all_matches destruct_sig_matcher. Ltac destruct_sig' := destruct_all_matches' destruct_sig_matcher. -(** try to specialize all non-dependent hypotheses using [tac] *) +Ltac transparent_specialize_one H arg := + first [ let test := eval unfold H in H in idtac; + let H' := fresh in rename H into H'; pose (H' arg) as H; subst H' + | specialize (H arg) ]. + +(** try to specialize all non-dependent hypotheses using [tac], maintaining transparency *) Ltac specialize_by' tac := idtac; match goal with - | [ H : ?A -> ?B |- _ ] => let H' := fresh in assert (H' : A) by tac; specialize (H H'); clear H' + | [ H : ?A -> ?B |- _ ] => + let H' := fresh in + assert (H' : A) by tac; + transparent_specialize_one H H'; + try clear H' (* if [H] was transparent, [H'] will remain *) end. Ltac specialize_by tac := repeat specialize_by' tac. -- cgit v1.2.3