diff options
Diffstat (limited to 'theories/Program/Equality.v')
| -rw-r--r-- | theories/Program/Equality.v | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 2f0185eac..d678757d9 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -37,11 +37,6 @@ Ltac unblock_goal := unfold block in *. 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]] [A]. -Implicit Arguments JMeq_refl [[A] [x]] [A]. - (** Do something on an heterogeneous equality appearing in the context. *) Ltac on_JMeq tac := |