13 files changed, 274 insertions, 4 deletions
diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v
index 9c11d19c27..b50371386f 100644
--- a/test-suite/ltac2/compat.v
+++ b/test-suite/ltac2/compat.v
@@ -40,6 +40,67 @@ Fail Ltac1.run (ltac1val:(x |- idtac) 0).
 Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))).
 Abort.
 
+(** Check value-returning FFI *)
+
+(* A dummy CPS wrapper in Ltac1 *)
+Ltac arg k :=
+match goal with
+| [ |- ?P ] => k P
+end.
+
+Ltac2 testeval v :=
+  let r := { contents := None } in
+  let k c :=
+    let () := match Ltac1.to_constr c with
+    | None => ()
+    | Some c => r.(contents) := Some c
+    end in
+    (* dummy return value *)
+    ltac1val:(idtac)
+  in
+  let tac := ltac1val:(arg) in
+  let () := Ltac1.apply tac [Ltac1.lambda k] (fun _ => ()) in
+  match r.(contents) with
+  | None => fail
+  | Some c => if Constr.equal v c then () else fail
+  end.
+
+Goal True.
+Proof.
+testeval 'True.
+Abort.
+
+Goal nat.
+Proof.
+testeval 'nat.
+Abort.
+
+(* CPS towers *)
+Ltac2 testeval2 tac :=
+  let fail _ := Control.zero Not_found in
+  let cast c := match Ltac1.to_constr c with
+  | None => fail ()
+  | Some c => c
+  end in
+  let f x y z :=
+    let x := cast x in
+    let y := cast y in
+    let z := cast z in
+    Ltac1.of_constr constr:($x $y $z)
+  in
+  let f := Ltac1.lambda (fun x => Ltac1.lambda (fun y => Ltac1.lambda (fun z => f x y z))) in
+  Ltac1.apply tac [f] Ltac1.run.
+
+Goal False -> True.
+Proof.
+ltac1:(
+let ff := ltac2:(tac |- testeval2 tac) in
+ff ltac:(fun k =>
+  let c := k (fun (n : nat) (i : True) (e : False) => i) O I in
+  exact c)
+).
+Qed.
+
 (** Test calls to Ltac2 from Ltac1 *)
 
 Set Default Proof Mode "Classic".
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 01564e7f25..984ac4e527 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -74,7 +74,9 @@ fun '{{n, m, p}} => n + m + p
 fun '(D n m p q) => n + m + p + q
      : J -> nat
 The command has indeed failed with message:
-The constructor D (in type J) expects 3 arguments.
+Once notations are expanded, the resulting constructor D (in type J) is
+expected to be applied to no arguments while it is actually applied to
+1 argument.
 lem1 = 
 fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
      : forall k : nat * nat, k = k
@@ -181,3 +183,51 @@ end
 File "stdin", line 253, characters 4-5:
 Warning: Unused variable B catches more than one case.
 [unused-pattern-matching-variable,pattern-matching]
+The command has indeed failed with message:
+Application of arguments to a recursive notation not supported in patterns.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 3 arguments.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 1 argument.
+The command has indeed failed with message:
+The constructor D' (in type J') is expected to be applied to 4 arguments (or
+6 arguments when including variables for local definitions) while it is
+actually applied to 5 arguments.
+fun x : J' bool (true, true) =>
+match x with
+| D' _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e
+end
+     : J' bool (true, true) -> {x0 : nat & x0 = x0}
+fun x : J' bool (true, true) =>
+match x with
+| @D' _ _ _ _ n _ p _ => n + p
+end
+     : J' bool (true, true) -> nat
+The command has indeed failed with message:
+Application of arguments to a recursive notation not supported in patterns.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 3 arguments.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 1 argument.
+The command has indeed failed with message:
+The constructor D' (in type J') is expected to be applied to 3 arguments (or
+4 arguments when including variables for local definitions) while it is
+actually applied to 2 arguments.
+The command has indeed failed with message:
+The constructor D' (in type J') is expected to be applied to 3 arguments (or
+4 arguments when including variables for local definitions) while it is
+actually applied to 5 arguments.
+fun x : J' bool (true, true) =>
+match x with
+| @D' _ _ _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e
+end
+     : J' bool (true, true) -> {x0 : nat & x0 = x0}
+fun x : J' bool (true, true) =>
+match x with
+| @D' _ _ _ _ n _ p _ => (n, p)
+end
+     : J' bool (true, true) -> nat * nat
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 2d8a8b359c..0cb3ac3ddc 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -254,3 +254,33 @@ Definition bar (f : foo) :=
   end.
 
 End Wish12762.
+
+Module ConstructorArgumentsNumber.
+
+Arguments cons {A} _ _.
+
+Inductive J' A {B} (C:=(A*B)%type) (c:C) := D' : forall n {m}, let p := n+m in m=m -> J' A c.
+
+Unset Asymmetric Patterns.
+
+Fail Check fun x => match x with (y,z) w => y+z+w end.
+Fail Check fun x => match x with cons y z w => 0 | nil => 0 end.
+Fail Check fun x => match x with cons y => 0 | nil => 0 end.
+
+(* Missing a let-in to be in let-in mode *)
+Fail Check fun x => match x with D' _ _ n p e => 0 end.
+Check fun x : J' bool (true,true) => match x with D' _ _ n e => existT (fun x => eq x x) _ e end.
+Check fun x : J' bool (true,true) => match x with D' _ _ _ n p e => n+p end.
+
+Set Asymmetric Patterns.
+
+Fail Check fun x => match x with (y,z) w => y+z+w end.
+Fail Check fun x => match x with cons y z w => 0 | nil => 0 end.
+Fail Check fun x => match x with cons y => 0 | nil => 0 end.
+
+Fail Check fun x => match x with D' n _ => 0 end.
+Fail Check fun x => match x with D' n m p e _ => 0 end.
+Check fun x : J' bool (true,true) => match x with D' n m e => existT (fun x => eq x x) m e end.
+Check fun x : J' bool (true,true) => match x with D' n m p e => (n,p) end.
+
+End ConstructorArgumentsNumber.
diff --git a/test-suite/output/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out
index 5b67f632c9..b80345108e 100644
--- a/test-suite/output/RecordFieldErrors.out
+++ b/test-suite/output/RecordFieldErrors.out
@@ -11,4 +11,4 @@ This record defines several times the field foo.
 The command has indeed failed with message:
 This record defines several times the field unit.
 The command has indeed failed with message:
-unit: Not a projection of inductive t.
+unit: Not a projection.
diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v
index 27aa07822b..ff817c31aa 100644
--- a/test-suite/output/RecordFieldErrors.v
+++ b/test-suite/output/RecordFieldErrors.v
@@ -35,4 +35,4 @@ acceptable and seems an unlikely mistake. *)
 
 Fail Check {| foo := tt;
               unit := tt |}.
-(* unit: Not a projection of inductive t. *)
+(* unit: Not a projection. *)
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 0fbb4f4c11..95b6c6ee95 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -162,6 +162,9 @@ When declaring multiple axioms in one command, only the first is allowed a unive
 foo@{i} = Type@{M.i} -> Type@{i}
      : Type@{max(M.i+1,i+1)}
 (* i |=  *)
+Type@{u0} -> Type@{UnivBinders.64}
+     : Type@{max(u0+1,UnivBinders.64+1)}
+(* {UnivBinders.64} |=  *)
 bind_univs.mono = 
 Type@{bind_univs.mono.u}
      : Type@{bind_univs.mono.u+1}
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index ed6e90b2a6..9539e34cfe 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -161,6 +161,16 @@ Module Notas.
 
 End Notas.
 
+Module NoAutoNames.
+  Monomorphic Universe u0.
+
+  (* The anonymous universe doesn't get a name (names are only
+     invented at the end of a definition/inductive) so no need to
+     qualify u0. *)
+  Check (Type@{u0} -> Type).
+
+End NoAutoNames.
+
 (* Universe binders survive through compilation, sections and modules. *)
 Require TestSuite.bind_univs.
 Print bind_univs.mono.
diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v
index 6f7be22fa0..7ab218a27a 100644
--- a/test-suite/output/bug_12908.v
+++ b/test-suite/output/bug_12908.v
@@ -7,7 +7,7 @@ Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
 End A.
 
 Module B.
-(* Test that an overriden scoped notation is deactivated *)
+(* Test that an overridden scoped notation is deactivated *)
 Infix "*" := mult' : nat_scope.
 Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
 End B.
diff --git a/test-suite/output/bug_13595.out b/test-suite/output/bug_13595.out
new file mode 100644
index 0000000000..2423b77b55
--- /dev/null
+++ b/test-suite/output/bug_13595.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+Tactic failure: Goal is solvable by congruence but some arguments are missing.
+  Try "congruence with ((Triple a _ _)) ((Triple d c _))",
+  replacing metavariables by arbitrary terms.
diff --git a/test-suite/output/bug_13595.v b/test-suite/output/bug_13595.v
new file mode 100644
index 0000000000..27a9ebe15d
--- /dev/null
+++ b/test-suite/output/bug_13595.v
@@ -0,0 +1,8 @@
+Inductive Cube:Set :=| Triple: nat -> nat -> nat -> Cube.
+
+Theorem incomplete :forall a b c d : nat,Triple a = Triple b->Triple d c = Triple d b->a = c.
+Proof.
+  Fail congruence.
+  intros.
+  congruence with ((Triple a a a)) ((Triple d c a)).
+Qed.
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 465b3eb8c0..90c1b308f2 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -89,3 +89,16 @@ Check fun x:Ind bool nat =>
   match x in Ind _ X Y Z return Z with
   | y => (true,0)
   end.
+
+(* A check that multi-implicit arguments work *)
+
+Check fun x : {True}+{False} => match x with left _ _ => 0 | right _ _ => 1 end.
+Check fun x : {True}+{False} => match x with left _ => 0 | right _ => 1 end.
+
+(* Check that Asymmetric Patterns does not apply to the in clause *)
+
+Inductive expr {A} : A -> Type := intro : forall {n:nat} (a:A), n=n -> expr a.
+Check fun (x:expr true) => match x in expr n return n=n with intro _ _ => eq_refl end.
+Set Asymmetric Patterns.
+Check fun (x:expr true) => match x in expr n return n=n with intro _ a _ => eq_refl a end.
+Unset Asymmetric Patterns.
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 232ac17cbf..e678fc7882 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1882,3 +1882,60 @@ Check match O in nat return nat with O => O | _ => O end.
 (* Checking that aliases are substituted in the correct order *)
 
 Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0.
+
+(* Checking use of argument scopes *)
+
+Module Intern.
+
+Inductive I (A:Type) := C : nat -> let a:=0 in bool -> list bool -> bool -> I A.
+
+Close Scope nat_scope.
+Notation "0" := true : bool_scope.
+Notation "0" := nil : list_scope.
+Notation C' := @C (only parsing).
+Notation C'' := C (only parsing).
+Notation C''' := (C _ 0) (only parsing).
+
+Set Asymmetric Patterns.
+
+Check fun x => match x with C 0 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C 0 _ 0 0 0 => O | _ => O end. (* was not supported *)
+
+Check fun x => match x with C' 0 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C' _ 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C' 0 _ 0 0 0 => O | _ => O end. (* was not supported *)
+Check fun x => match x with C' _ _ 0 0 0 => O | _ => O end. (* was pre 8.5 bug *)
+
+Check fun x => match x with C'' 0 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C'' _ 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C'' 0 _ 0 0 0 => O | _ => O end. (* was not supported *)
+Check fun x => match x with C'' _ _ 0 0 0 => O | _ => O end. (* was pre 8.5 bug *)
+
+Check fun x => match x with C''' 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C''' _ 0 0 0 => O | _ => O end. (* was not supported  *)
+
+Unset Asymmetric Patterns.
+Arguments C {A} _ {x} _ _.
+
+Check fun x => match x with C 0 0 0 => O | _ => O end. (* was ok *)
+Check fun x => match x with C 0 _ 0 0 => O | _ => O end. (* was wrong scope on last argument with let-in *)
+
+Check fun x => match x with C' _ 0 _ 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with C' _ 0 _ 0 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with C'' _ 0 0 => O | _ => O end. (* was ok *)
+Check fun x => match x with C'' _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with C''' 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with C''' _ 0 0 => O | _ => O end. (* works by miscount compensating *)
+
+Check fun x => match x with (@C _ 0) _ 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with (@C _ 0) _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with @C _ 0 _ 0 0 => O | _ => O end. (* was ok *)
+Check fun x => match x with @C _ 0 _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with (@C) _ O _ 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with (@C) _ O _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+End Intern.
diff --git a/test-suite/success/cbv_let.v b/test-suite/success/cbv_let.v
new file mode 100644
index 0000000000..861a73a64e
--- /dev/null
+++ b/test-suite/success/cbv_let.v
@@ -0,0 +1,34 @@
+Record T : Type := Build_T { f : unit; g := pair f f; }.
+
+Definition t : T := {| f := tt; |}.
+
+Goal match t return unit with Build_T f g => f end = tt.
+Proof.
+cbv.
+reflexivity.
+Qed.
+
+Goal match t return prod unit unit with Build_T f g => g end = pair tt tt.
+Proof.
+cbv.
+reflexivity.
+Qed.
+
+Goal forall (x : T),
+  match x return prod unit unit with Build_T f g => g end =
+  pair match x return unit with Build_T f g => fst g end match x return unit with Build_T f g => snd g end.
+Proof.
+cbv.
+destruct x.
+reflexivity.
+Qed.
+
+Record U : Type := Build_U { h := tt }.
+
+Definition u : U := Build_U.
+
+Goal match u with Build_U h => h end = tt.
+Proof.
+cbv.
+reflexivity.
+Qed.