Merge branch 'v8.5' into v8.6

3 files changed, 243 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4762.v b/test-suite/bugs/closed/4762.v
new file mode 100644
index 0000000000..7a87b07a8e
--- /dev/null
+++ b/test-suite/bugs/closed/4762.v
@@ -0,0 +1,24 @@
+Inductive myand (P Q : Prop) := myconj : P -> Q -> myand P Q.
+
+Lemma foo P Q R : R = myand P Q -> P -> Q -> R.
+Proof. intros ->; constructor; auto. Qed.
+
+Hint Extern 0 (myand _ _) => eapply foo; [reflexivity| |] : test1.
+
+Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R).
+Proof.
+  intros.
+  eauto with test1.
+Qed.
+
+Hint Extern 0 =>
+  match goal with
+  | |- myand _ _ => eapply foo; [reflexivity| |]
+  end : test2.
+
+Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R).
+Proof.
+  intros.
+  eauto with test2. (* works *)
+Qed.
+
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
index 209b2bc26f..dbb9e09a43 100644
--- a/test-suite/output/subst.out
+++ b/test-suite/output/subst.out
@@ -26,6 +26,19 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
   x, y : nat
   Hx : x = 0
   Hy : y = 0
@@ -39,6 +52,45 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
   H1 : 0 = 1
   HA : True
   H2 : 0 = 2
@@ -52,6 +104,58 @@
   y, z : nat
   Hy : y = 0
   Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
   HA : True
   H3 : y = 3
   HB : True
@@ -75,6 +179,19 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
   x, y : nat
   Hx : x = 0
   Hy : y = 0
@@ -88,6 +205,45 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  HB : True
+  H4 : z = 4
+  H3 : 0 = 3
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
   HA, HB : True
   H4 : 0 = 4
   H3 : 0 = 3
@@ -95,3 +251,55 @@
   H2 : 0 = 2
   ============================
   True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  HB : True
+  H4 : z = 4
+  H3 : 0 = 3
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v
index e48aa6bb28..91bdd03e02 100644
--- a/test-suite/output/subst.v
+++ b/test-suite/output/subst.v
@@ -45,4 +45,15 @@ Show.
 trivial.
 Qed.
 
+(* A bug revealed by OCaml 4.03 warnings *)
+Goal forall y, let x:=0 in y=x -> y=y.
+intros * H;
+subst.
+Fail clear H. (* Was working *)
+Abort.
 
+Goal forall y, let x:=0 in y=x -> y=y.
+intros * H;
+subst.
+Fail clear H. (* Was failing before fix *)
+Abort.