3 files changed, 8 insertions, 3 deletions
diff --git a/test-suite/output/EqNotation.out b/test-suite/output/EqNotation.out
new file mode 100644
index 0000000000..41500a75b9
--- /dev/null
+++ b/test-suite/output/EqNotation.out
@@ -0,0 +1,3 @@
+The command has indeed failed with message:
+Cannot infer the implicit parameter A of eq whose type is 
+"Type".
diff --git a/test-suite/output/EqNotation.v b/test-suite/output/EqNotation.v
new file mode 100644
index 0000000000..21076472b8
--- /dev/null
+++ b/test-suite/output/EqNotation.v
@@ -0,0 +1,2 @@
+(* should mention "the implicit parameter A of eq" *)
+Fail Type (forall x, x = x).
diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out
index ca56f032ff..f02e442be5 100644
--- a/test-suite/output/Show.out
+++ b/test-suite/output/Show.out
@@ -1,10 +1,10 @@
-3 subgoals (ID 31)
+3 subgoals (ID 29)
   
   H : 0 = 0
   ============================
   1 = 1
 
-subgoal 2 (ID 35) is:
+subgoal 2 (ID 33) is:
  1 = S (S m')
-subgoal 3 (ID 22) is:
+subgoal 3 (ID 20) is:
  S (S n') = S m