Merge branch 'v8.5'

2 files changed, 6 insertions, 0 deletions

diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
new file mode 100644
index 0000000000..e912003f03
--- /dev/null
+++ b/test-suite/output/Inductive.out
@@ -0,0 +1,3 @@
+The command has indeed failed with message:
+Last occurrence of "list'" must have "A" as 1st argument in
+ "A -> list' A -> list' (A * A)%type".
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v
new file mode 100644
index 0000000000..8db8956e32
--- /dev/null
+++ b/test-suite/output/Inductive.v
@@ -0,0 +1,3 @@
+Fail Inductive list' (A:Set) : Set :=
+| nil' : list' A
+| cons' : A -> list' A -> list' (A*A).