| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
When comparing 2 irrelevant universes [u] and [v] we add a "weak
constraint" [UWeak(u,v)] to the UState. Then at minimization time a
weak constraint between unrelated universes where one is flexible
causes them to be unified.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative
inductive would try to generate a constraint [i = j] and use
cumulativity only if this resulted in an inconsistency. This is
confusingly different from the behaviour with [Type] and means
cumulativity can only be used to lift between universes related by
strict inequalities. (This isn't a kernel restriction so there might
be some workaround to send the kernel the right constraints, but
not in a nice way.)
See modified test for more details of what is now possible.
Technical notes:
When universe constraints were inferred by comparing the shape of
terms without reduction, cumulativity was not used and so too-strict
equality constraints were generated. Then in order to use cumulativity
we had to make this comparison fail to fall back to full conversion.
When unifiying 2 instances of a cumulative inductive type, if there
are any Irrelevant universes we try to unify them if they are
flexible.
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
Following up on #6791, we remove the option "Tactic Pattern Unification"
|
| | | | |
|
| | |/
|/| |
|
| |/ |
|
| | |
|
| |
|
|
|
|
| |
This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
|
| |
|
|
|
|
|
|
| |
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.
|
Gaëtan Gilbert
Maxime Dénès
Emilio Jesus Gallego Arias
Théo Zimmermann
Pierre-Marie Pédrot
Matthieu Sozeau
Hugo Herbelin
Guillaume Melquiond
Gaetan Gilbert