| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
This brings more compatibility with handling of mutual primitive records
in the kernel.
|
| |\ |
|
| | |
| |
| |
| |
| | |
When called by auto, `simple apply` still does not respect `Opaque`
because of compatibility issues.
|
| |/
|
|
|
|
|
| |
We use an option type instead of returning a pair with a boolean. Indeed, the
boolean being true was always indicating that the returned value was unchanged.
The previous API was somewhat error-prone, and I don't understand why it was
designed this way in the first place.
|
| |\
| |
| |
| | |
tactic unification.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
The old unification engine was using the unfiltered environment when a
context had been cleared, leading to an ill-typed goal.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
Should it be removed? The underlying
`universe_subst -> constr -> constr`
seems like it could be useful for plugins but where would the
substitution be from?
|
| | | |
| | |
| | |
| | | |
clear_hyps remain with no alternative
|
| | | |
| | |
| | |
| | |
| | |
| | | |
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
| | | |
| | |
| | |
| | |
| | | |
This is more efficient in general, because Termops.dependent doesn't take
advantage of the knowledge of its pattern argument.
|
| |/ / |
|
| |/ |
|
| |
|
|
|
|
|
| |
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.
|
Pierre-Marie Pédrot
Maxime Dénès
Matthieu Sozeau
Gaëtan Gilbert
Emilio Jesus Gallego Arias
Hugo Herbelin
Théo Zimmermann
Guillaume Melquiond