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 /interp/notation_ops.ml | |
| 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 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions