Ensuring that patterns of the form pat/constr move the hypotheses replacing

an initial hypothesis hyp at the same position in the context.

Ensuring the same for "apply c in hyp as pat".

Ensuring that "pose proof (H ...) as H" does not change the position of H.

1 files changed, 25 insertions, 11 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f2185d7dfe..bbee0a2a79 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -848,6 +848,14 @@ let get_next_hyp_position id gl =
   in
   aux (Proofview.Goal.hyps (Proofview.Goal.assume gl))
 
+let get_previous_hyp_position id gl =
+  let rec aux dest = function
+  | [] -> raise (RefinerError (NoSuchHyp id))
+  | (hyp,_,_) :: right ->
+    if Id.equal hyp id then dest else aux (MoveAfter hyp) right
+  in
+  aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
+
 let intro_replacing id =
   Proofview.Goal.enter begin fun gl ->
   let next_hyp = get_next_hyp_position id gl in
@@ -2160,8 +2168,9 @@ let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
           (n+List.length ids) tac l)
   | IntroAction pat ->
       intro_then_gen (make_tmp_naming avoid l pat)
-	MoveLast true false
+	destopt true false
         (intro_pattern_action loc (b || not (List.is_empty l)) false pat thin
+          destopt
           (fun thin bound' -> intro_patterns_core b avoid ids thin destopt bound' 0
             (fun ids thin ->
               intro_patterns_core b avoid ids thin destopt bound (n+1) tac l)))
@@ -2185,7 +2194,7 @@ and intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l =
 	destopt true false
         (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l)
 
-and intro_pattern_action loc b style pat thin tac id = match pat with
+and intro_pattern_action loc b style pat thin destopt tac id = match pat with
   | IntroWildcard ->
       tac ((loc,id)::thin) None []
   | IntroOrAndPattern ll ->
@@ -2198,7 +2207,8 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
 	(rewrite_hyp style l2r id)
         (tac thin None [])
   | IntroApplyOn (f,(loc,pat)) ->
-      let naming,tac_ipat = prepare_intros_loc loc (IntroIdentifier id) pat in
+      let naming,tac_ipat =
+        prepare_intros_loc loc (IntroIdentifier id) destopt pat in
       Proofview.Goal.enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
@@ -2211,16 +2221,16 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
           sigma
       end
 
-and prepare_intros_loc loc dft = function
+and prepare_intros_loc loc dft destopt = function
   | IntroNaming ipat ->
       prepare_naming loc ipat,
-      (fun _ -> Proofview.tclUNIT ())
+      (fun id -> Proofview.V82.tactic (move_hyp id destopt))
   | IntroAction ipat ->
       prepare_naming loc dft,
       (let tac thin bound =
-        intro_patterns_core true [] [] thin MoveLast bound 0
+        intro_patterns_core true [] [] thin destopt bound 0
           (fun _ l -> clear_wildcards l) in
-      fun id -> intro_pattern_action loc true true ipat [] tac id)
+      fun id -> intro_pattern_action loc true true ipat [] destopt tac id)
   | IntroForthcoming _ -> user_err_loc
       (loc,"",str "Introduction pattern for one hypothesis expected.")
 
@@ -2246,9 +2256,9 @@ let intros_patterns = function
 (*   Forward reasoning    *)
 (**************************)
 
-let prepare_intros dft = function
+let prepare_intros dft destopt = function
   | None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ())
-  | Some (loc,ipat) -> prepare_intros_loc loc dft ipat
+  | Some (loc,ipat) -> prepare_intros_loc loc dft destopt ipat
 
 let ipat_of_name = function
   | Anonymous -> None
@@ -2259,8 +2269,9 @@ let head_ident c =
    if isVar c then Some (destVar c) else None
 
 let assert_as first hd ipat t =
-  let naming,tac = prepare_intros IntroAnonymous ipat in
+  let naming,tac = prepare_intros IntroAnonymous MoveLast ipat in
   let repl = do_replace hd naming in
+  let tac = if repl then (fun id -> Proofview.tclUNIT ()) else tac in
   if first then assert_before_then_gen repl naming t tac
   else assert_after_then_gen repl naming t tac
 
@@ -2271,13 +2282,16 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
   let tac (naming,lemma) tac id =
     apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
       naming id lemma tac in
-  let naming,ipat_tac = prepare_intros (IntroIdentifier id) ipat in
+  Proofview.Goal.enter begin fun gl ->
+  let destopt = get_previous_hyp_position id gl in
+  let naming,ipat_tac = prepare_intros (IntroIdentifier id) destopt ipat in
   let lemmas_target, last_lemma_target =
     let last,first = List.sep_last lemmas in
     List.map (fun lem -> (NamingMustBe (dloc,id),lem)) first, (naming,last)
   in
   (* We chain apply_in_once, ending with an intro pattern *)
   List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
+  end
 
 (*
   if sidecond_first then