Merge branch 'v8.5' into v8.6

3 files changed, 1 insertions, 220 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index bb8723dfe6..5b07d3ec3b 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -100,7 +100,7 @@ let coqide_cmd_checks (loc,ast) =
   if is_debug ast then
     user_error "Debug mode not available within CoqIDE";
   if is_known_option ast then
-    Feedback.msg_warning (strbrk"This will not work. Use CoqIDE display menu instead");
+    Feedback.msg_warning (strbrk"This will not work. Use CoqIDE view menu instead");
   if Vernac.is_navigation_vernac ast || is_undo ast then
     Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead");
   if is_query ast then
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
index dbb9e09a43..209b2bc26f 100644
--- a/test-suite/output/subst.out
+++ b/test-suite/output/subst.out
@@ -26,19 +26,6 @@
   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
@@ -52,45 +39,6 @@
   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
@@ -104,58 +52,6 @@
   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
@@ -179,19 +75,6 @@
   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
@@ -205,45 +88,6 @@
   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
@@ -251,55 +95,3 @@
   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 91bdd03e02..e48aa6bb28 100644
--- a/test-suite/output/subst.v
+++ b/test-suite/output/subst.v
@@ -45,15 +45,4 @@ 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.