9 files changed, 255 insertions, 4 deletions
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/StringSyntaxPrimitive.out b/test-suite/output/StringSyntaxPrimitive.out
new file mode 100644
index 0000000000..131975c760
--- /dev/null
+++ b/test-suite/output/StringSyntaxPrimitive.out
@@ -0,0 +1,20 @@
+"abc"
+     : intList
+"abc"
+     : intList
+mk_intList [97%int63; 98%int63; 99%int63]
+     : intList
+"abc"
+     : intArray
+"abc"
+     : intArray
+     = "abc"
+     : nestArray
+"abc"
+     : nestArray
+"100"
+     : floatList
+"100"
+     : floatList
+mk_floatList [1%float; 0%float; 0%float]
+     : floatList
diff --git a/test-suite/output/StringSyntaxPrimitive.v b/test-suite/output/StringSyntaxPrimitive.v
new file mode 100644
index 0000000000..23ef082013
--- /dev/null
+++ b/test-suite/output/StringSyntaxPrimitive.v
@@ -0,0 +1,139 @@
+Require Import Coq.Lists.List.
+Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii.
+Require Coq.Array.PArray Coq.Floats.PrimFloat.
+Require Import Coq.Numbers.BinNums Coq.Numbers.Cyclic.Int63.Int63.
+
+Set Printing Depth 100000.
+Set Printing Width 1000.
+
+Close Scope char_scope.
+Close Scope string_scope.
+
+(* Notations for primitive integers inside polymorphic datatypes *)
+Module Test1.
+  Inductive intList := mk_intList (_ : list int).
+  Definition i63_from_byte (b : byte) : int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)).
+  Definition i63_to_byte (i : int) : byte :=
+      match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end.
+
+  Definition to_byte_list '(mk_intList a) := List.map i63_to_byte a.
+
+  Definition from_byte_list (xs : list byte) : intList:=
+    mk_intList (List.map i63_from_byte xs).
+
+  Declare Scope intList_scope.
+  Delimit Scope intList_scope with intList.
+
+  String Notation intList from_byte_list to_byte_list : intList_scope.
+
+  Open Scope intList_scope.
+  Import List.ListNotations.
+  Check mk_intList [97; 98; 99]%int63%list.
+  Check "abc"%intList.
+
+  Definition int' := int.
+  Check mk_intList (@cons int' 97 [98; 99])%int63%list.
+End Test1.
+
+Import PArray.
+
+(* Notations for primitive arrays *)
+Module Test2.
+  Inductive intArray := mk_intArray (_ : array int).
+
+  Definition i63_from_byte (b : byte) : Int63.int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)).
+  Definition i63_to_byte (i : Int63.int) : byte :=
+  match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end.
+
+  Definition i63_to_nat x := BinInt.Z.to_nat (Int63.to_Z x).
+  Local Definition nat_length {X} (x : array X) :nat := i63_to_nat (length x).
+
+  Local Fixpoint list_length_i63 {A} (xs : list A) :int :=
+            match xs with
+            | nil => 0
+            | cons _ xs => 1 + list_length_i63 xs
+            end.
+
+  Definition to_byte_list '(mk_intArray a) :=
+    ((fix go (n : nat) (i : Int63.int) (acc : list byte) :=
+        match n with
+        | 0 => acc
+        | S n => go n (i - 1) (cons (i63_to_byte a.[i]) acc)
+        end) (nat_length a) (length a - 1) nil)%int63.
+
+  Definition from_byte_list (xs : list byte) :=
+    (let arr := make (list_length_i63 xs) 0 in
+    mk_intArray ((fix go i xs acc :=
+        match xs with
+        | nil => acc
+        | cons x xs => go (i + 1) xs (acc.[i <- i63_from_byte x])
+        end) 0 xs arr))%int63.
+
+  Declare Scope intArray_scope.
+  Delimit Scope intArray_scope with intArray.
+
+  String Notation intArray from_byte_list to_byte_list : intArray_scope.
+
+  Open Scope intArray_scope.
+  Check mk_intArray ( [| 97; 98; 99 | 0|])%int63%array.
+  Check "abc"%intArray.
+
+End Test2.
+
+(* Primitive arrays inside primitive arrays *)
+Module Test3.
+
+  Inductive nestArray := mk_nestArray (_ : array (array int)).
+  Definition to_byte_list '(mk_nestArray a) :=
+    ((fix go (n : nat) (i : Int63.int) (acc : list byte) :=
+        match n with
+        | 0 => acc
+        | S n => go n (i - 1) (cons (Test2.i63_to_byte a.[i].[0]) acc)
+        end) (Test2.nat_length a) (length a - 1) nil)%int63.
+
+  Definition from_byte_list (xs : list byte) :=
+    (let arr := make (Test2.list_length_i63 xs) (make 0 0) in
+    mk_nestArray ((fix go i xs acc :=
+        match xs with
+        | nil => acc
+        | cons x xs => go (i + 1) xs (acc.[i <- make 1 (Test2.i63_from_byte x)])
+        end) 0 xs arr))%int63.
+
+  Declare Scope nestArray_scope.
+  Delimit Scope nestArray_scope with nestArray.
+
+  String Notation nestArray from_byte_list to_byte_list : nestArray_scope.
+
+  Open Scope nestArray_scope.
+  Eval cbv in mk_nestArray ( [| make 1 97; make 1 98; make 1 99 | make 0 0|])%int63%array.
+  Check "abc"%nestArray.
+End Test3.
+
+
+
+(* Notations for primitive floats inside polymorphic datatypes *)
+Module Test4.
+  Import PrimFloat.
+  Inductive floatList := mk_floatList (_ : list float).
+  Definition float_from_byte (b : byte) : float :=
+    if Byte.eqb b "0"%byte then PrimFloat.zero else PrimFloat.one.
+  Definition float_to_byte (f : float) : byte :=
+    if PrimFloat.is_zero f then "0" else "1".
+  Definition to_byte_list '(mk_floatList a) := List.map float_to_byte a.
+
+  Definition from_byte_list (xs : list byte) : floatList:=
+    mk_floatList (List.map float_from_byte xs).
+
+  Declare Scope floatList_scope.
+  Delimit Scope floatList_scope with floatList.
+
+  String Notation floatList from_byte_list to_byte_list : floatList_scope.
+
+  Open Scope floatList_scope.
+  Import List.ListNotations.
+  Check mk_floatList [97; 0; 0]%float%list.
+  Check "100"%floatList.
+
+  Definition float' := float.
+  Check mk_floatList (@cons float' 1 [0; 0])%float%list.
+End Test4.
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.