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.

4 files changed, 73 insertions, 12 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
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 074004fa12..55b666b723 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -548,3 +548,14 @@ apply (foo ?y).
 Grab Existential Variables.
 exact 0.
 Qed.
+
+(* Test position of new hypotheses when using "apply ... in ... as ..." *)
+Goal (True -> 0=0 /\ True) -> True -> False -> True/\0=0.
+intros H H0 H1.
+apply H in H0 as (a,b).
+(* clear H1:False *) match goal with H:_ |- _ => clear H end.
+split.
+- (* use b:True *) match goal with H:_ |- _ => exact H end.
+- (* clear b:True *) match goal with H:_ |- _ => clear H end.
+  (* use a:0=0 *) match goal with H:_ |- _ => exact H end.
+Qed.
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 9443d01e3b..4959b65788 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -33,3 +33,21 @@ Goal True -> True -> True.
 intros _ ?.
 exact H.
 Qed.
+
+(* A short test about introduction pattern pat/c *)
+Goal (True -> 0=0) -> True /\ False -> 0=0.
+intros H (H1/H,_).
+exact H1.
+Qed.
+
+(* A test about bugs in 8.5beta2 *)
+Goal (True -> 0=0) -> True /\ False -> False -> 0=0.
+intros H H0 H1.
+destruct H0 as (a/H,_).
+(* Check that H0 is removed (was bugged in 8.5beta2) *)
+Fail clear H0.
+(* Check position of newly created hypotheses when using pat/c (was
+   left at top in 8.5beta2) *)
+match goal with H:_ |- _ => clear H end. (* clear H1:False *)
+match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *)
+Qed.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index c5f032beb0..3faa1ca43a 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -45,4 +45,22 @@ specialize eq_trans with _ a b c. intros _.
 (* Anomaly: Evar ?88 was not declared. Please report. *)
 *)
 
-Abort.
\ No newline at end of file
+Abort.
+
+(* Test use of pose proof and assert as a specialize *)
+
+Goal True -> (True -> 0=0) -> False -> 0=0.
+intros H0 H H1.
+pose proof (H I) as H.
+(* Check that the hypothesis is in 2nd position by removing the top one *)
+match goal with H:_ |- _ => clear H end.
+match goal with H:_ |- _ => exact H end.
+Qed.
+
+Goal True -> (True -> 0=0) -> False -> 0=0.
+intros H0 H H1.
+assert (H:=H I).
+(* Check that the hypothesis is in 2nd position by removing the top one *)
+match goal with H:_ |- _ => clear H end.
+match goal with H:_ |- _ => exact H end.
+Qed.