| Age | Commit message (Collapse) | Author |
|---|
|
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
|
|
|
|
|
|
|
|
|
|
|
`internal_ghost` was an artifact to ease porting of the ml4 rules. Now
that the location is optional we can finally get rid of it.
|
|
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
|
Now it is a private field, locations are optional.
|
|
One case missing due the TACTIC EXTEND macro.
|
|
|
|
|
|
The syntax is: TACTIC EXTEND foo AT LEVEL i
This commit makes it possible to define tacticals like the ssreflect
arrow without having to resort to GEXTEND statements and intepretation
hacks.
Note that it simply makes accessible through the ML interface what Tactic
Notation already supports:
Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...
|
|
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|
