| Age | Commit message (Collapse) | Author |
|---|
|
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
|
|
|
|
Reviewed-by: gares
|
|
Reviewed-by: mattam82
Reviewed-by: gares
Ack-by: SkySkimmer
|
|
tactics.
Reviewed-by: ppedrot
|
|
projection expansion.
Reviewed-by: ejgallego
|
|
We additionally check that occurrence 0 is invalid in simpl at,
unfold at, etc.
|
|
No need to call the whole whd_gen machinery when a simple matching over
a term would suffice.
Note that this changes a bit the semantics, but I suspect that the previous
code was buggy. Indeed, whd_nored also pushes cases and fixpoints on the
stack, so that an applied canonical projection inside such a context would
also match. But the caller in unification performs an approximate check where
the term needs to be an application or a projection, which would prevent
such complex situations most of the time, e.g. it would work with a dummy
commutative cut but not their corresponding vanilla match.
|
|
There functions export the internal stack representation. The only real user
is unification, which is suffering from major performance issues due to the
naive representation of substitutions in processes.
|
|
|
|
This was revealed on the rewriter contrib with the compact-case-repr branch.
|
|
|
|
cleanup of constrintern.ml
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
|
|
Namely, WrongNumargInductive and WrongNumargConstructor.
|
|
We also simplify the whole process of interpretation of cases pattern
on the way.
|
|
|
|
constants/inductives/constructors
Reviewed-by: SkySkimmer
|
|
Reviewed-by: mattam82
|
|
|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
|
|
To tie the knot (since the evar depends on the evar type and the
source of the evar type of the evar), we use an "update_source"
function.
An alternative could be to provide a function to build both an evar
with its evar type directly in evd.ml...
|
|
erroneously caught
Reviewed-by: ppedrot
|
|
Fixes #7430 and fixes #10968
This commit makes the following changes:
- Add an exception `Signal` used to convert OCaml signals to exceptions.
`Signal` is registered as critical in `CErrors` to avoid being caught in the
wrong `with` clauses.
- Make `Control.timeout` into a safer interface based on `option` instead of
exceptions.
- Modify `tclTIMEOUT` to fail with `CErrors.Timeout` instead of
`Logic_monad.Tac_timeout`, as was already advertised in the ocamldoc documentation.
- Removes `Logic_monad.Tac_timeout` altogether because it no longer has a use.
|
|
|
|
semantic.
|
|
|
|
|
|
Also includes minor layout or code changes.
|
|
We also align their type on (more) standard invariants.
|
|
|
|
primitive projection was wrongly supposed to be already inferred
Reviewed-by: gares
|
|
template poly
Reviewed-by: gares
Reviewed-by: herbelin
|
|
This is to make more explicit that arguments of the projection are not
kept.
We seize this opportunity to use QGlobRef equality on GlobRef.
|
|
type.
This was a case where expand_projections was calling find_mrectype
which was expecting the argument of the projection to be an inductive.
We could have ensured that this type is at least the appropriate
inductive applied to fresh evars, but this expand_projections was in
practice used for checking the applicability of canonical structures
and the unifiability of the parameters of the projections is anyway a
consequence of the unifiability of the principal argument of the
projections. So, the latter is enough.
|
|
locating fix
Reviewed-by: gares
|
|
Reviewed-by: gares
|
|
of the definition of the metas
Reviewed-by: mattam82
|
|
of unification
Reviewed-by: mattam82
|
|
|
|
We ensure that when imitation stops to be possible, we postpone an
equation of the type of the subterm (and not of the arbitrary type of
an evar possibly depending on this subterm).
|
|
It remains to accept resolving Type(u)<=Prop for u arbitrary sort variable.
|
|
See 742ef62fe8050a6865d06bd644e30cbec0e7eb02
Fix #13366
Fix #9809
|
|
sort elimination constraints
Reviewed-by: gares
|
|
(solve_simple_eqn).
The bug was that an assumption could be interpreted as a local
definition and wrongly expanded.
It triggered rarely because it involved mixing let-ins and
local assumptions + imitation under binders.
|
|
Even though it is not strongly supposed to be raised.
|
|
handler in NotFoundInstance
Reviewed-by: ejgallego
|
|
Fixes #13266 (see #12675, 8641cb7385).
|
|
In Evar := C[Meta] problems of unification.ml, and C[ ] contains
binders, Meta was wrongly considered by pose_all_metas_as_evars as
under these binders (while Metas are always defined in the initial
context of the unification problem).
|
