Merge branch 'v8.6'

2 files changed, 42 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v
new file mode 100644
index 0000000000..831e8fb507
--- /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 0000000000..d28303b8ab
--- /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.