Fix super_nsatz tactic to be better about ordering

See also #13.

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'
+  | .. ].