diff options
| author | Gaëtan Gilbert | 2020-02-20 16:50:24 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-25 13:43:23 +0100 |
| commit | 0dab087b10598f79ffa4f907c6d93fb7932e1c5b (patch) | |
| tree | 7a49e711046ea7ef5071f448da669c546c5409c9 /theories/Init | |
| parent | 1bc8cd6390a3208659d563b1363f9bc0d87643a0 (diff) | |
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".
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Logic.v | 8 |
1 files changed, 4 insertions, 4 deletions
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. |