diff options
Diffstat (limited to 'src/Util/Tactics.v')
-rw-r--r-- | src/Util/Tactics.v | 22 |
1 files changed, 22 insertions, 0 deletions
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' + | .. ]. |