| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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".
|
|
We remove the emacs-specific printing code from the core of Coq, now
`-emacs` is a printing flag controlled by the toplevel.
|
|
This allows a better control on the name to give to an evar and, in
particular, to address the issue about naming produced by "epose
proof" in one of the comment of Zimmi48 at PR #248 (see file names.v).
Incidentally updating output of Show output test (evar numbers shifted).
|
|
|
