aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program/Equality.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program/Equality.v')
-rw-r--r--theories/Program/Equality.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 37c17aa9a..2f0185eac 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -39,8 +39,8 @@ Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
(** Notation for the single element of [x = x] and [x ~= x]. *)
-Implicit Arguments eq_refl [[A] [x]].
-Implicit Arguments JMeq_refl [[A] [x]].
+Implicit Arguments eq_refl [[A] [x]] [A].
+Implicit Arguments JMeq_refl [[A] [x]] [A].
(** Do something on an heterogeneous equality appearing in the context. *)