Merge remote-tracking branch 'origin/v8.5' into trunk

3 files changed, 58 insertions, 1 deletions

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 074004fa1..55b666b72 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 9443d01e3..ae1694c58 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -33,3 +33,31 @@ 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.
+
+Goal (True -> 0=0) -> True -> 0=0.
+intros H H1/H.
+exact H1.
+Qed.
+
+Goal forall n, n = S n -> 0=0.
+intros n H/n_Sn.
+destruct H.
+Qed.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index c5f032beb..3faa1ca43 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.