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 +++---
 theories/Init/Logic.v                 | 8 ++++----
 6 files changed, 18 insertions(+), 13 deletions(-)
 create mode 100644 test-suite/output/EqNotation.out
 create mode 100644 test-suite/output/EqNotation.v

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
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 9698737d33..aa376b780a 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -352,10 +352,6 @@ Inductive eq (A:Type) (x:A) : A -> Prop :=
 
 where "x = y :> A" := (@eq A x y) : type_scope.
 
-Notation "x = y" := (x = y :>_) : type_scope.
-Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
-Notation "x <> y" := (x <> y :>_) : type_scope.
-
 Arguments eq {A} x _.
 Arguments eq_refl {A x} , [A] x.
 
@@ -363,6 +359,10 @@ Arguments eq_ind [A] x P _ y _.
 Arguments eq_rec [A] x P _ y _.
 Arguments eq_rect [A] x P _ y _.
 
+Notation "x = y" := (eq x y) : type_scope.
+Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
+Notation "x <> y" := (~ (x = y)) : type_scope.
+
 Hint Resolve I conj or_introl or_intror : core.
 Hint Resolve eq_refl: core.
 Hint Resolve ex_intro ex_intro2: core.
-- 
cgit v1.2.3