6 files changed, 167 insertions, 36 deletions
diff --git a/test-suite/output/RecordProjParameter.out b/test-suite/output/RecordProjParameter.out
new file mode 100644
index 0000000000..91ae4b6511
--- /dev/null
+++ b/test-suite/output/RecordProjParameter.out
@@ -0,0 +1,33 @@
+t1 : Atype -> forall a : Type, a
+
+t1 is not universe polymorphic
+Arguments t1 _ _%type_scope
+t1 is transparent
+Expands to: Constant RecordProjParameter.t1
+t3 : forall a0 : Atype, t2 a0
+
+t3 is not universe polymorphic
+t3 is transparent
+Expands to: Constant RecordProjParameter.t3
+u1 : Btype -> forall b b0 : Type, b * b0
+
+u1 is not universe polymorphic
+Arguments u1 _ (_ _)%type_scope
+u1 is transparent
+Expands to: Constant RecordProjParameter.u1
+u3 : forall b1 : Btype, u2 b1
+
+u3 is not universe polymorphic
+u3 is transparent
+Expands to: Constant RecordProjParameter.u3
+v1 : Ctype -> forall c0 : Type, c0
+
+v1 is not universe polymorphic
+Arguments v1 _ _%type_scope
+v1 is transparent
+Expands to: Constant RecordProjParameter.v1
+v3 : forall c : Ctype, v2 c
+
+v3 is not universe polymorphic
+v3 is transparent
+Expands to: Constant RecordProjParameter.v3
diff --git a/test-suite/output/RecordProjParameter.v b/test-suite/output/RecordProjParameter.v
new file mode 100644
index 0000000000..8b892c694c
--- /dev/null
+++ b/test-suite/output/RecordProjParameter.v
@@ -0,0 +1,21 @@
+Record Atype : Type :=
+  { t1 : forall (a : Type), a
+  ; t2 : Type
+  ; t3 : t2 }.
+About t1.
+About t3.
+
+Record Btype : Type :=
+  { u1 : forall (b : Type) (b0 : Type), b * b0
+  ; u2 : Type
+  ; u3 : u2 }.
+About u1.
+About u3.
+
+Record Ctype : Type :=
+  { v1 : forall (c0 : Type), c0
+  ; v2 : Type
+  ; v3 : v2
+  }.
+About v1.
+About v3.
diff --git a/test-suite/output/ltac2_deprecated.out b/test-suite/output/ltac2_deprecated.out
new file mode 100644
index 0000000000..d17b719bcd
--- /dev/null
+++ b/test-suite/output/ltac2_deprecated.out
@@ -0,0 +1,12 @@
+File "stdin", line 13, characters 11-14:
+Warning: Ltac2 definition foo is deprecated. test_definition
+[deprecated-ltac2-definition,deprecated]
+- : unit = ()
+File "stdin", line 14, characters 11-14:
+Warning: Ltac2 alias bar is deprecated. test_notation
+[deprecated-ltac2-alias,deprecated]
+- : unit = ()
+File "stdin", line 15, characters 11-14:
+Warning: Ltac2 definition qux is deprecated. test_external
+[deprecated-ltac2-definition,deprecated]
+- : 'a array -> int = <fun>
diff --git a/test-suite/output/ltac2_deprecated.v b/test-suite/output/ltac2_deprecated.v
new file mode 100644
index 0000000000..9598a5979c
--- /dev/null
+++ b/test-suite/output/ltac2_deprecated.v
@@ -0,0 +1,15 @@
+Require Import Ltac2.Ltac2.
+
+#[deprecated(note="test_definition")]
+Ltac2 foo := ().
+
+#[deprecated(note="test_notation")]
+Ltac2 Notation bar := ().
+
+#[deprecated(note="test_external")]
+Ltac2 @ external qux : 'a array -> int := "ltac2" "array_length".
+(* Randomly picked external function *)
+
+Ltac2 Eval foo.
+Ltac2 Eval bar.
+Ltac2 Eval qux.
diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
index 48368c7ede..6bf03d30d3 100644
--- a/test-suite/output/relaxed_ambiguous_paths.out
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -1,13 +1,24 @@
-File "stdin", line 10, characters 0-28:
+File "stdin", line 13, characters 0-29:
 Warning:
-New coercion path [ac; cd] : A >-> D is ambiguous with existing 
-[ab; bd] : A >-> D. [ambiguous-paths,typechecker]
-[ab] : A >-> B
-[ac] : A >-> C
-[ab; bd] : A >-> D
-[bd] : B >-> D
-[cd] : C >-> D
-File "stdin", line 26, characters 0-28:
+New coercion path [g1; f2] : A >-> B' is ambiguous with existing 
+[f1; g2] : A >-> B'. [ambiguous-paths,typechecker]
+File "stdin", line 14, characters 0-29:
+Warning:
+New coercion path [h1; f3] : B >-> C' is ambiguous with existing 
+[f2; h2] : B >-> C'. [ambiguous-paths,typechecker]
+[f1] : A >-> A'
+[g1] : A >-> B
+[f1; g2] : A >-> B'
+[g1; h1] : A >-> C
+[f1; g2; h2] : A >-> C'
+[g2] : A' >-> B'
+[g2; h2] : A' >-> C'
+[f2] : B >-> B'
+[h1] : B >-> C
+[f2; h2] : B >-> C'
+[h2] : B' >-> C'
+[f3] : C >-> C'
+File "stdin", line 33, characters 0-28:
 Warning:
 New coercion path [ab; bc] : A >-> C is ambiguous with existing 
 [ac] : A >-> C. [ambiguous-paths,typechecker]
@@ -17,6 +28,19 @@ New coercion path [ab; bc] : A >-> C is ambiguous with existing
 [bc] : B >-> C
 [bc; cd] : B >-> D
 [cd] : C >-> D
+File "stdin", line 50, characters 0-28:
+Warning:
+New coercion path [ab; bc] : A >-> C is ambiguous with existing 
+[ac] : A >-> C. [ambiguous-paths,typechecker]
+File "stdin", line 51, characters 0-28:
+Warning:
+New coercion path [ba; ab] : B >-> B is not definitionally an identity function.
+New coercion path [ab; ba] : A >-> A is not definitionally an identity function.
+[ambiguous-paths,typechecker]
+[ab] : A >-> B
+[ac] : A >-> C
+[ba] : B >-> A
+[bc] : B >-> C
 [B_A] : B >-> A
 [C_A] : C >-> A
 [D_A] : D >-> A
@@ -31,7 +55,7 @@ New coercion path [ab; bc] : A >-> C is ambiguous with existing
 [D_B; B_A'] : D >-> A'
 [D_B] : D >-> B
 [D_C] : D >-> C
-File "stdin", line 121, characters 0-86:
+File "stdin", line 147, characters 0-86:
 Warning:
 New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing 
 [D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker]
@@ -44,15 +68,15 @@ New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
 [D_B; B_A'] : D >-> A'
 [D_B] : D >-> B
 [D_C] : D >-> C
-File "stdin", line 130, characters 0-47:
+File "stdin", line 156, characters 0-47:
 Warning:
 New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT is not definitionally an identity function.
 [ambiguous-paths,typechecker]
-File "stdin", line 131, characters 0-64:
+File "stdin", line 157, characters 0-64:
 Warning:
 New coercion path [unwrap_list; wrap_list] : LIST >-> LIST is not definitionally an identity function.
 [ambiguous-paths,typechecker]
-File "stdin", line 132, characters 0-51:
+File "stdin", line 158, characters 0-51:
 Warning:
 New coercion path [unwrap_Type; wrap_Type] : TYPE >-> TYPE is not definitionally an identity function.
 [ambiguous-paths,typechecker]
diff --git a/test-suite/output/relaxed_ambiguous_paths.v b/test-suite/output/relaxed_ambiguous_paths.v
index 41322045f2..182e155273 100644
--- a/test-suite/output/relaxed_ambiguous_paths.v
+++ b/test-suite/output/relaxed_ambiguous_paths.v
@@ -1,13 +1,20 @@
 Module test1.
 Section test1.
 
-Variable (A B C D : Type).
-Variable (ab : A -> B) (bd : B -> D) (ac : A -> C) (cd : C -> D).
-
-Local Coercion ab : A >-> B.
-Local Coercion bd : B >-> D.
-Local Coercion ac : A >-> C.
-Local Coercion cd : C >-> D.
+Variable (A B C A' B' C' : Type).
+Variable (f1 : A -> A') (f2 : B -> B') (f3 : C -> C').
+Variable (g1 : A -> B) (g2 : A' -> B') (h1 : B -> C) (h2 : B' -> C').
+
+Local Coercion g1 : A >-> B.
+Local Coercion g2 : A' >-> B'.
+Local Coercion h1 : B >-> C.
+Local Coercion h2 : B' >-> C'.
+Local Coercion f1 : A >-> A'.
+Local Coercion f2 : B >-> B'.
+Local Coercion f3 : C >-> C'.
+(* [g1; h1; f3], [f1; g2; h2] : A >-> C' should not be reported as ambiguous  *)
+(* paths because they are redundant with `[g1; f2], [f1; g2] : A >-> B'` and  *)
+(* `[h1; f3], [f2; h2] : B >-> C'`.                                           *)
 
 Print Graph.
 
@@ -24,8 +31,8 @@ Local Coercion ac : A >-> C.
 Local Coercion cd : C >-> D.
 Local Coercion ab : A >-> B.
 Local Coercion bc : B >-> C.
-(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be shown as ambiguous paths  *)
-(* here because they are redundant with `[ab; bc], [ac] : A >-> C`.           *)
+(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be reported as ambiguous     *)
+(* paths because they are redundant with `[ab; bc], [ac] : A >-> C`.          *)
 
 Print Graph.
 
@@ -34,6 +41,25 @@ End test2.
 
 Module test3.
 Section test3.
+
+Variable (A B C : Type).
+Variable (ab : A -> B) (ba : B -> A) (ac : A -> C) (bc : B -> C).
+
+Local Coercion ac : A >-> C.
+Local Coercion bc : B >-> C.
+Local Coercion ab : A >-> B.
+Local Coercion ba : B >-> A.
+(* `[ba; ac], [bc] : B >-> C` should not be reported as ambiguous paths       *)
+(* because they are redundant with `[ab; bc], [ac] : A >-> C` and             *)
+(* `[ba; ab] : B >-> B`.                                                      *)
+
+Print Graph.
+
+End test3.
+End test3.
+
+Module test4.
+Section test4.
 Variable (A : Type) (P Q : A -> Prop).
 
 Record B := {
@@ -57,11 +83,11 @@ Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d).
 
 Print Graph.
 
-End test3.
-End test3.
+End test4.
+End test4.
 
-Module test4.
-Section test4.
+Module test5.
+Section test5.
 
 Variable (A : Type) (P Q : A -> Prop).
 
@@ -89,11 +115,11 @@ Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d).
 
 Print Graph.
 
-End test4.
-End test4.
+End test5.
+End test5.
 
-Module test5.
-Section test5.
+Module test6.
+Section test6.
 
 Variable (A : Type) (P Q : A -> Prop).
 
@@ -123,18 +149,18 @@ Local Coercion D_C (d : D) : C true :=
 
 Print Graph.
 
-End test5.
-End test5.
+End test6.
+End test6.
 
-Module test6.
+Module test7.
 Record > NAT := wrap_nat { unwrap_nat :> nat }.
 Record > LIST (T : Type) := wrap_list { unwrap_list :> list T }.
 Record > TYPE := wrap_Type { unwrap_Type :> Type }.
-End test6.
+End test7.
 
-Module test7.
+Module test8.
 Set Primitive Projections.
 Record > NAT_prim := wrap_nat { unwrap_nat :> nat }.
 Record > LIST_prim (T : Type) := wrap_list { unwrap_list :> list T }.
 Record > TYPE_prim := wrap_Type { unwrap_Type :> Type }.
-End test7.
+End test8.