| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | |_|/ / /
|/| | | | |
|
| |\ \ \ \ \
| |_|_|_|/
|/| | | | |
|
| |\ \ \ \ \ |
|
| | |_|_|_|/
|/| | | |
| | | | | |
I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| | | | | | | |
|
| | |_|_|_|/
|/| | | | |
|
| | |_|/ /
|/| | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \
| |/ / /
|/| | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \ |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
a flag suspectingly renamed in a clearer way
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This exports two functions:
- declare_reduction_effect: to declare a hook to be applied when some
constant are visited during the execution of some reduction functions
(primarily cbv, but also cbn, simpl, hnf, ...).
- set_reduction_effect: to declare a constant on which a given effect
hook should be called.
Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin.
Added support for printing effect in functions of tacred.ml.
|
| | | | | | |
|
| | |_|_|/
|/| | | |
|
| | |/ /
|/| |
| | |
| | | |
I didn't rename the test file to `fiat` as IMHO it is not worth the noise.
|
| |\ \ \ |
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.
Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.
Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | | |
Constrintern.pf_global returns a global_reference, not a constr,
adapt plugins accordingly, properly registering universes where
necessary.
|
| |\ \ \ |
|
| | | | | |
|
| | |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We move Coqlib to library in preparation for the late binding of
Gallina-level references. Placing `Coqlib` in `library/` is convenient
as some components such as pretyping need to depend on it.
By moving we lose the ability to locate references by syntactic
abbreviations, but IMHO it makes to require ML code to refer to
a true constant instead of an abbreviation/notation.
Unfortunately this change means that we break the `Coqlib`
API (providing a compatibility function is not possible), however we
do so for a good reason.
The main changes are:
- move `Coqlib` to `library/`.
- remove reference -> term from `Coqlib`. In particular, clients will
have different needs with regards to universes/evar_maps, so we
force them to call the (not very safe) `Universes.constr_of_global`
explicitly so the users are marked.
- move late binding of impossible case from `Termops` to
`pretying/Evarconv`. Remove hook.
- `Coqlib.find_reference` doesn't support syntactic abbreviations
anymore.
- remove duplication of `Coqlib` code in `Program`.
- remove duplication of `Coqlib` code in `Ltac.Rewrite`.
- A special note about bug 5066 and commit 6e87877 . This case
illustrates the danger of duplication in the code base; the solution
chosen there was to transform the not-found anomaly into an error
message, however the general policy was far from clear. The long
term solution is indeed make `find_reference` emit `Not_found` and
let the client handle the error maybe non-fatally. (so they can test
for constants.
|
Maxime Dénès
Pierre Letouzey
Pierre-Marie Pédrot
Jason Gross
Matej Košík
Gaëtan Gilbert
Thomas Sibut-Pinote
Jason Gross
Emilio Jesus Gallego Arias
Hugo Herbelin
Matthieu Sozeau