| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | |/ /
| | | |
| | | |
| | | |
| | | | |
Any users of this API should coordinate with the ongoing work in PRs
numbered #459 and #566.
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which
this PR solves, I propose to remove support for non-synchronous
options.
It seems the few uses of `optsync = false` we legacy and shouldn't
have any impact.
Moreover, non synchronous options may create particularly tricky
situations as for instance, they won't be propagated to workers.
|
| | |\ \ \ \
| | |/ / /
| |/| | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This fixes the discrepancy between "rewrite H with (1 := x)"
and "setoid_rewrite H with (1 := x)".
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:
```
Goal Type.
⋮
Save id.
```
has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.
We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.
It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
|
| | |/ / /
| | | |
| | | |
| | | |
| | | |
| | | | |
Remove a space before colon.
Remove the use of term mandatory
(this closes https://coq.inria.fr/bugs/show_bug.cgi?id=3994).
|
| | | | | |
|
| | |/ / |
|
| | |\ \ |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |\ \ \ |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | |/ / /
|/| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The only remaining use was applied on the unfold tactic, and the behaviours
of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced
by their argument tactic.
|
| |/ / /
| | |
| | |
| | | |
The only use in Equality is reimplemented in the new engine.
|
| |\ \ \ |
|
| | | | | |
|
| |/ / / |
|
| |/ /
| |
| |
| | |
Also remove obvious comments.
|
| |\ \ |
|
| | |\ \ |
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This broke the build of iris-coq in the EConstr branch. Each time you
use unsafe_type_of, I loose a night of sleep, so please stop.
|
| |\ \ \ \ |
|
| | |/ / / |
|
| | |/ /
| | |
| | |
| | |
| | |
| | | |
We make apparent in the API that the implicit tactic is set or not. This was
costing a lot in Pretyping for no useful reason, as it is almost always unset
and the default implementation was just failing immediately.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- We avoid unnecessary use of Pp -> string conversion functions.
and the creation of intermediate buffers on logging.
- We rename local functions that share the name with the Coq stdlib,
this is usually dangerous as if the normal function is removed, code
may pick up the one in the stdlib, with different semantics.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
The code was assuming that Proofview.tclFOCUS could raise a
CList.IndexOutOfRange exception but this isn't the case.
The focusing functions already catch this exception and
raises an algebraic exception within the tactic mechanism.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | | |
Now they are useless because all of the primitives are (should?) be
evar-insensitive.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
This is now useless as this returns evar-constrs, so that all functions acting
on them should be insensitive to evar-normalization.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
|
| | | |
| | |
| | |
| | |
| | | |
This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.
|
| | | | |
|
| | | | |
|
Emilio Jesus Gallego Arias
Hugo Herbelin
Matthieu Sozeau
Maxime Dénès
Cyprien Mangin
Théo Zimmermann
Pierre-Marie Pédrot
Gaetan Gilbert
Matej Košík