From 0dab087b10598f79ffa4f907c6d93fb7932e1c5b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 20 Feb 2020 16:50:24 +0100
Subject: Use implicit arguments in notations for eq.

This gives IMO slightly nicer errors when the type cannot be inferred,
ie
~~~coq
Type (forall x, x = x).
~~~
says "cannot infer the implicit parameter A of eq" instead of "cannot
infer this placeholder".
---
 test-suite/output-coqtop/ShowGoal.out | 6 +++---
 test-suite/output-coqtop/ShowGoal.v   | 6 +++---
 test-suite/output/EqNotation.out      | 3 +++
 test-suite/output/EqNotation.v        | 2 ++
 test-suite/output/Show.out            | 6 +++---
 5 files changed, 14 insertions(+), 9 deletions(-)
 create mode 100644 test-suite/output/EqNotation.out
 create mode 100644 test-suite/output/EqNotation.v

(limited to 'test-suite')

diff --git a/test-suite/output-coqtop/ShowGoal.out b/test-suite/output-coqtop/ShowGoal.out
index 2eadd22db8..42d9ff31e9 100644
--- a/test-suite/output-coqtop/ShowGoal.out
+++ b/test-suite/output-coqtop/ShowGoal.out
@@ -52,19 +52,19 @@ x < 1 subgoal
   ============================
   i = i
 
-x < goal ID 16 at state 5
+x < goal ID 13 at state 5
   
   i : nat
   ============================
   i = ?j /\ ?j = ?k /\ i = ?k
 
-x < goal ID 16 at state 7
+x < goal ID 13 at state 7
   
   i : nat
   ============================
   i = i /\ i = ?k /\ i = ?k
 
-x < goal ID 16 at state 9
+x < goal ID 13 at state 9
   
   i : nat
   ============================
diff --git a/test-suite/output-coqtop/ShowGoal.v b/test-suite/output-coqtop/ShowGoal.v
index 9545254770..80996eb169 100644
--- a/test-suite/output-coqtop/ShowGoal.v
+++ b/test-suite/output-coqtop/ShowGoal.v
@@ -6,6 +6,6 @@ Proof using.
     trivial.
   split.
     trivial.
-Show Goal 16 at 5.
-Show Goal 16 at 7.
-Show Goal 16 at 9.
+Show Goal 13 at 5.
+Show Goal 13 at 7.
+Show Goal 13 at 9.
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
-- 
cgit v1.2.3