Merge branch 'v8.6'

5 files changed, 36 insertions, 5 deletions

diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 05eeaac631..bd9240476f 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -17,7 +17,7 @@ Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
 Arguments fcomp {_ _ _}%type_scope f g x /.
 About fcomp.
 Definition volatile := fun x : nat => x.
-Arguments volatile /.
+Arguments volatile / _.
 About volatile.
 Set Implicit Arguments.
 Section S1.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 3488cb3056..1633ad9765 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,9 +1,20 @@
+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.
 Argument A renamed to B.
-The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
-Argument A renamed to T.
+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]
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
@@ -110,6 +121,9 @@ 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]
 The command has indeed failed with message:
 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 b6fbeb6ec7..e42c983361 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.
-Fail Arguments identity T _ _.
+Arguments identity T _ _.
 Arguments eq_refl A x : assert.
 Arguments eq_refl {B y}, [B] y : rename.
 
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index db464fd07e..751d5fcc48 100644
--- a/test-suite/output/PrintModule.out
+++ b/test-suite/output/PrintModule.out
@@ -2,3 +2,4 @@ Module N : S with Definition T := nat := M
 
 Module N : S with Module T := K := M
 
+Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 999d9a9862..5f30f7cda6 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -32,3 +32,19 @@ Module N : S with Module T := K := M.
 Print Module N.
 
 End BAR.
+
+Module QUX.
+
+Module Type Test.
+  Parameter t : Type.
+End Test.
+
+Module Type Func (T:Test).
+  Parameter x : T.t.
+End Func.
+
+Module Shortest_path (T : Test).
+Print Func.
+End Shortest_path.
+
+End QUX.