From 5329170c85614f943e34652426181759990f6036 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jun 2016 12:34:46 -0700 Subject: Fix super_nsatz tactic to be better about ordering See also #13. --- src/Util/Tactics.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'src/Util/Tactics.v') diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 6826f638e..a911ca48d 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -228,3 +228,25 @@ Ltac destruct_sig_matcher HT := end. Ltac destruct_sig := destruct_all_matches destruct_sig_matcher. Ltac destruct_sig' := destruct_all_matches' destruct_sig_matcher. + +(** If [tac_in H] operates in [H] and leaves side-conditions before + the original goal, then + [side_conditions_before_to_side_conditions_after tac_in H] does + the same thing to [H], but leaves side-conditions after the + original goal. *) +Ltac side_conditions_before_to_side_conditions_after tac_in H := + let HT := type of H in + let HTT := type of HT in + let H' := fresh in + rename H into H'; + let HT' := fresh in + evar (HT' : HTT); + cut HT'; + [ subst HT'; intro H + | tac_in H'; + [ .. + | subst HT'; eexact H' ] ]; + [ (* We preserve the order of the hypotheses. We need to do this + here, after evars are instantiated, and not above. *) + move H after H'; clear H' + | .. ]. -- cgit v1.2.3