Merge PR #11644: Use implicit arguments in notations for eq.

Reviewed-by: herbelin

6 files changed, 18 insertions, 13 deletions

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.