| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
| |
This ensures that the API is self-contained and is, well, an API.
Before this patch, the contents of `API.mli` bore little relation with
what was used by the plugins [example: `Metasyntax` in tacentries.ml].
Many missing types had to be added.
A sanity check of the `API.mli` file can be done with:
`ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
|
| | |
|
| | |
|
| |
|
|
|
|
| |
This string contains the base-10 representation of the number (big endian)
Note that some inner parsing stuff still uses bigints, see egramcoq.ml
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
evars.
This is for consistency with the rest of the language. For instance,
"eremember" and "epose" are supposed to refer to terms occurring in
the goal, hence not leaving evars, hence in general pointless.
Eventually, I guess that "e" should be a modifier (see e.g. the
discussion at #3872), or the difference is removed.
|
| |
|
|
| |
a goal with unresolved evars.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.
This provides significantly clearer code for the AST, and is robust
wrt attributes.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| |/
|
|
|
|
|
|
|
| |
This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.
Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.
|
| |
|
|
|
|
|
|
| |
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
|
| |
|
|
|
|
|
| |
- Adding a better location in the "apply" on the fly pattern.
- Printing statement of lemma and of hypothesis.
Was suggested by discussion at wish report #5390.
|
|
|
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.
|
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Pierre Letouzey
Matej Košík
Hugo Herbelin