Merge branch 'v8.6'

8 files changed, 77 insertions, 26 deletions

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b8c07512f..ba85286dd 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v
new file mode 100644
index 000000000..831e8fb50
--- /dev/null
+++ b/test-suite/bugs/closed/5127.v
@@ -0,0 +1,15 @@
+Fixpoint arrow (n: nat) :=
+  match n with
+  | S n => bool -> arrow n
+  | O => bool
+  end.
+
+Fixpoint apply (n : nat) : arrow n -> bool :=
+  match n return arrow n -> bool with
+  | S n => fun f => apply _ (f true)
+  | O => fun x => x
+  end.
+
+Axiom f : arrow 10000.
+Definition v : bool := Eval compute in apply _ f.
+Definition w : bool := Eval vm_compute in v.
diff --git a/test-suite/bugs/closed/5161.v b/test-suite/bugs/closed/5161.v
new file mode 100644
index 000000000..d28303b8a
--- /dev/null
+++ b/test-suite/bugs/closed/5161.v
@@ -0,0 +1,27 @@
+(* Check that the presence of binders with type annotation do not
+   prevent the recursive binder part to be found *)
+
+From Coq Require Import Utf8.
+
+Delimit Scope C_scope with C.
+Global Open Scope C_scope.
+
+Delimit Scope uPred_scope with I.
+
+Definition FORALL {T : Type} (f : T → Prop) : Prop := ∀ x, f x.
+
+Notation "∀ x .. y , P" :=
+  (FORALL (λ x, .. (FORALL (λ y, P)) ..)%I)
+  (at level 200, x binder, y binder, right associativity) : uPred_scope.
+Infix "∧" := and : uPred_scope.
+
+(* The next command fails with
+   In recursive notation with binders, Φ is expected to come without type.
+   I would expect this notation to work fine, since the ∀ does support
+   type annotation.
+*)
+Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
+  (∀ Φ : _ → _,
+      (∀ x, .. (∀ y, Q ∧ Φ pat) .. ))%I
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  {{{ x .. y ;  pat ,  Q } } }") : uPred_scope.
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 2c7b04c62..a2ee2d4c8 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -101,4 +101,4 @@ Error: Unknown interpretation for notation "$".
 w 3 true = tt
      : Prop
 The command has indeed failed with message:
-Error: Extra argument _.
+Error: Extra arguments: _, _.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 1633ad976..9d90de47c 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,20 +1,12 @@
-File "stdin", line 1, characters 0-36:
-Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
-[arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be
+specified.
 Argument A renamed to B.
 File "stdin", line 2, characters 0-25:
-Warning: Ignoring rename of A into T. Only implicit arguments can be renamed.
-[arguments-ignore-rename-nonimpl,vernacular]
-File "stdin", line 2, characters 0-25:
-Warning: This command is just asserting the number and names of arguments of
-identity. If this is what you want add ': assert' to silence the warning. If
-you want to clear implicit arguments add ': clear implicits'. If you want to
-clear notation scopes add ': clear scopes' [arguments-assert,vernacular]
-File "stdin", line 4, characters 0-40:
-Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
-[arguments-ignore-rename-nonimpl,vernacular]
+Warning: This command is just asserting the names of arguments of identity.
+If this is what you want add ': assert' to silence the warning. If you want
+to clear implicit arguments add ': clear implicits'. If you want to clear
+notation scopes add ': clear scopes' [arguments-assert,vernacular]
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
@@ -112,18 +104,16 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-Error: All arguments lists must declare the same names.
+Error: Arguments lists should agree on names they provide.
 The command has indeed failed with message:
-Error: The following arguments are not declared: x.
+Error: Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
 Error: Arguments names must be distinct.
 The command has indeed failed with message:
 Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
-Error: Extra argument y.
-File "stdin", line 53, characters 0-26:
-Warning: Ignoring rename of x into s. Only implicit arguments can be renamed.
-[arguments-ignore-rename-nonimpl,vernacular]
+Error: Extra arguments: y.
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be
+specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index e42c98336..2d14c94ac 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -1,5 +1,5 @@
 Fail Arguments eq_refl {B y}, [B] y.
-Arguments identity T _ _.
+Arguments identity A _ _.
 Arguments eq_refl A x : assert.
 Arguments eq_refl {B y}, [B] y : rename.
 
@@ -46,9 +46,9 @@ About myplus.
 Check @myplus.
 
 Fail Arguments eq_refl {F g}, [H] k.
-Fail Arguments eq_refl {F}, [F].
+Fail Arguments eq_refl {F}, [F] : rename.
 Fail Arguments eq_refl {F F}, [F] F.
-Fail Arguments eq {F} x [z].
+Fail Arguments eq {F} x [z] : rename.
 Fail Arguments eq {F} x z y.
 Fail Arguments eq {R} s t.
 
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index a7bde5ea3..1ff09e3af 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,5 +1,6 @@
 The command has indeed failed with message:
-Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
+Error:
+Ltac variable y depends on pattern variable name z which is not bound in current context.
 Ltac f x y z :=
   symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
    dependent z
diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v
index 976bec737..e25510cf0 100644
--- a/test-suite/success/clear.v
+++ b/test-suite/success/clear.v
@@ -13,3 +13,21 @@ Goal forall y z, (forall x:nat, x=y -> True) -> y=z -> True.
   reflexivity.
 Qed.
 
+Class A.
+
+Section Foo.
+
+  Variable a : A.
+
+  Goal A.
+    solve [typeclasses eauto].
+    Undo 1.
+    clear a.
+    try typeclasses eauto.
+    assert(a:=Build_A).
+    solve [ typeclasses eauto ].
+    Undo 2.
+    assert(b:=Build_A).
+    solve [ typeclasses eauto ].
+  Qed.
+End Foo.
\ No newline at end of file