| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
In current code, `Proofview.Goal.t` uses a phantom type to indicate
whether the goal was properly substituted wrt current `evar_map` or
not.
After the introduction of `EConstr`, this distinction should have
become unnecessary, thus we remove the phantom parameter from
`'a Proofview.Goal.t`. This may introduce some minor incompatibilities
at the typing level. Code-wise, things should remain the same.
We thus deprecate `assume`. In a next commit, we will remove
normalization as much as possible from the code.
|
| |
|
|
|
|
|
| |
We simply use a record and pack the rel and var substitutions in it. We also
properly compose variable substitutions.
Fixes #6534: Fresh variable generation in case of clash is buggy.
|
| |
|
|
|
|
|
|
|
| |
The exception needs to carry aroud a pair of `env, sigma` so printing
is correct. This gets rid of a few global calls, and it is IMO the
right thing to do.
While we are at it, we incorporate some fixes to a couple of
additional printing functions missing the `env, sigma` pair.
|
| |
|
|
|
|
|
|
|
|
|
| |
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | |_|/
|/| |
| | |
| | | |
Only in ml files that are not related to Coq commands
|
| | | | |
|
| | |/
|/| |
|
| |\ \
| |/
|/| |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | | |/
| | |
| | |
| | |
| | | |
It used to compute the dependencies of all undefined evars of the
evar_map, while only the dependencies of resolvable evars are necessary.
|
| | |/
| |
| |
| |
| | |
eval thunks once in prlist_sep_lastsep, make code clearer
add typeclass debug output test
|
| |/ |
|
| | |
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
sorting for the dependency order option.
|
| | |/
|/| |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Reminder of (some of) the reasons for removal:
- Despite the claim in sigma.mli, it does *not* prevent evar
leaks, something like:
fun env evd ->
let (evd',ev) = new_evar env evd in
(evd,ev)
will typecheck even with Sigma-like type annotations (with a proof of
reflexivity)
- The API stayed embryonic. Even typing functions were not ported to
Sigma.
- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
at all (despite still being so).
- There was no good story for higher order functions manipulating evar
maps. Without higher order, one can most of the time get away with
reusing the same name for the updated evar map.
- Most of the code doing complex things with evar maps was using unsafe
casts to sigma. This code should be fixed, but this is an orthogonal
issue.
Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | | |
It looks like `Class_tactics` forgot to register a couple of global
variables with the summary, thus creating problems on backtracking.
Fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5578
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | |
| | | |
Now we properly report NoApplicableEx/ReachedLimit and CannotUnify
exceptions that can be raised during resolution.
|
| |/ / |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
Today, both modes are controlled by a single flag, however this is a
bit misleading as is_silent really means "quiet", that is to say `coqc
-q` whereas "verbose" is Coq normal operation.
We also restore proper behavior of goal printing in coqtop on quiet
mode, thanks to @Matafou for the report.
|
| | |
| |
| |
| |
| |
| | |
The evarmap used by the heuristic could contain resolved evars, which could
lead to a failure of backtracking in the EConstr branch. This is experimental
and may be to costly.
|
| | |
| |
| |
| |
| | |
For now we only normalize sorts, and we leave instances for the next
commit.
|
| |\ \ |
|
| | |\| |
|
| | | |\
| | | |
| | | |
| | | | |
correctly as…
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
The underlying hint mode implementation was not using the evar-insensitive
API so that it resulted in strange bugs.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
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 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
Pierre-Marie Pédrot
Maxime Dénès
amblaf
Matej Košík
Théo Zimmermann
Matthieu Sozeau
Paul Steckler
Matthieu Sozeau
Hugo Herbelin
Gaetan Gilbert