| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
If a term is matched only against variables, it will not introduce a
"match" and thus, even if the term is of an inductive type, its
indices will not be taken into account in the current algorithm
(though one could imagine an algorithm which does an expansion
specially in order to filter on indices).
This allows to tell the unification not to use dependencies which the
pattern-matching algorithm is not able to exploit in practice.
See example in file 2733.v.
|
|
|
|
There were actually two broken things with VM + evars, the fixes are:
- Do not pass let-bound arguments to evars.
- Use the right order for evar arguments.
Native compilation seems to be suffering from the same shortcomings, I will
open a separate bug and adapt the PR.
|
|
The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
|
|
|
|
|
|
|
|
While we were adding a new field into `QuestionMark`, we
decided to go ahead and refactor the constructor to hold
an actual record. This record now holds the name, obligations, and
whether the evar represents a missing record field.
This is used to provide better error messages on missing record
fields.
|
|
We only ever call `reduction_effect_hook` on constants, so there's no
point allowing it to be declared with globrefs. There is also no point
using a constr map instead of constant map.
(Technically there was a call of the effect hook on projections, but
that can never match a globref so it was useless)
|
|
|
|
|
|
In #7607, dead code that used to handle non-dependent return predicates
was removed. This made the reification branch expecting non-functions
in predicates dead code. We fix this by using an assert instead.
|
|
|
|
|
|
|
|
(Universes and Evd)
|
|
compilers
|
|
constr in Constr
|
|
|
|
I believe this is legacy code due to a previous, more complex
representation of return predicates in the kernel.
|
|
|
|
This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.
Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
|
|
|
|
|
|
|
|
This brings more compatibility with handling of mutual primitive records
in the kernel.
|
|
This is a first step towards the acceptance of mutual record types in the
kernel.
|
|
It seems that lifting a term with a negative index is not equivalent to
strengthening it by applying to a dummy substitution. This looks suspicious
at best.
|
|
|
|
|
|
|
|
induction schemes
|
|
|
|
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
|
This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.
Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.
Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.
|
|
This field was not used inside the kernel and not used in
performance-critical code where caching is essential, so we extrude
the code that computes it out of the kernel.
|
|
|
|
This ensures that computations are shared as much as possible, mimicking
the "positive" records computational behavior if possible.
|
|
Avoid adding the same unification problem twice, module evar instantiation.
|
|
|
|
to anomaly)
|
|
in unification
|
|
names" warnings
|
|
Currently, if one of the inductives is non recursive, it defaults to a
case analysis schems taking fewer predicates and methods just for that
inductive. This irregularity prevents doing a combined scheme afterwards
to gather all eliminators into one, as combined scheme expects all the
eliminators to have the same predicates and methods. I have a use case
in building function graphs in Equations where some of the inductives
might not be recursive but I expect many other use cases could exist.
|
|
We move the last 3 types to more adequate places.
|
|
We move the "flag types" to its use place, and mark some arguments
with named parameters better.
|
