| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
|
| |\
| |
| |
| | |
arguments.
|
| | |
| |
| |
| | |
This is a follow-up on 866b449c497933a3ab1185c194d8d33a86c432f2.
|
| |/
|
|
|
| |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
| |
|
|
|
|
| |
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
|
| | |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | |/
| | |
| | |
| | | |
We do up to `Term` which is the main bulk of the changes.
|
| | |/
|/|
| |
| | |
This will allow to merge back `Names` with `API.Names`
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Formerly, mk_refgoals in logic.ml was applying full βι on new Meta-based goals.
We simulate part of this βι-normalization in pose_all_metas_as_evars.
I suspect that we don't βι-normalize goals more than in 8.4 by doing
that, since all Metas would have eventually gone to mk_refgoals, but
difficult to know for sure as there were probably metas turned to
evars (and hence a priori not βι-normalized) even when logic.ml was
used more pervasively.
However, βι-normalizing is a priori a better heuristic than no
βι-normalizing, independently of what it was in 8.4 and before (even
if, ideally, I would personally lean towards preferring a
"chirurgical" substitution with reduction only at the place of
substitution).
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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 it is a private field, locations are optional.
|
| |\ |
|
| | |
| |
| |
| |
| | |
Getting a key only needs to observe the root of a term. This hotspot was
observed in HoTT.
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| | |
For now we only normalize sorts, and we leave instances for the next
commit.
|
| | |
| |
| |
| | |
Was breaking e.g. fiat-crypto.
|
| | |
| |
| |
| |
| |
| | |
All functions where actually called with the second argument of the pending
problem being the current evar map. We simply remove this useless and
error-prone second component.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| | |
This is another perfomance-critical function in unification. Putting it in
the EConstr API was changing the heuristic, so better revert on that change.
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
It seems this is a performance-critical function for unification-heavy code.
In particular, tactics relying on meta unification suffered an important
penalty after this function was rewritten with the evar-insensitive API, as
witnessed e.g. by Ncring_polynom whose compilation time increased by ~30%.
I am not sure about the specification of this function, but it seems safer
to revert the changes and just do it the old way. It may even disappear if
we get rid of the old unification algorithm at some point.
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | |
| |
| |
| |
| | |
We make mli files look to what they were looking before the move to EConstr
by opening this module.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
Emilio Jesus Gallego Arias
Maxime Dénès
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Guillaume Melquiond
Gaetan Gilbert