| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
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.
|
|
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
|
|
|
|
|
|
|
|
|
|
|
vm_compute and native_compute (partial fix to #7068; also fixes #7076))
|
|
Instead of having a constant-based compilation of projections, we
generate them at the compilation time of the inductive block to which
they pertain.
|
|
|
|
When called by auto, `simple apply` still does not respect `Opaque`
because of compatibility issues.
|
|
Note that the normalization of the context of the return predicate was
not done by the native compilation but by the lazy machine. The patch
also "fixes" an anomaly in the case of an arity which was not in
canonical form as in:
Inductive A : nat -> id (nat->Type) := .
Eval native_compute in fun x => match x in A y z return y = z with end.
|
|
Note that the normalization of the context of the return predicate was
not done by the vm but by the lazy machine. The patch also "fixes" an
anomaly in the case of an arity which was not in canonical form as in:
Inductive A : nat -> id (nat->Type) := .
Eval vm_compute in fun x => match x in A y z return y = z with end.
|
|
pattern-matching names
|
|
|
|
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.
|
|
|
|
|
|
|
|
Continuing the interface cleanup we place `Constrexpr` in the
internalization module, which is the one that eliminates it.
This slims down `pretyping` considerably, including removing the
`Univdecls` module which existed only due to bad dependency ordering
in the first place. Thanks to @ Skyskimmer we also remove a duplicate
`univ_decl` definition among `Misctypes` and `UState`.
This is mostly a proof of concept yet as it depends on quite a few
patches of the tree. For sure some tweaks will be necessary, but it
should be good for review now.
IMO the tree is now in a state where we can could easy eliminate more
than 10 modules without any impact, IMHO this is a net saving API-wise
and would help people to understand the structure of the code better.
|
|
|
|
Instead of having the projection data in the constant data we have it
independently in the environment.
|
|
Close #7562.
[api] move hint_info ast to tactics.
|
|
We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.
Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.
The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.
|
|
|
|
We now have only two notions of environments in the kernel: env and
safe_env.
|
|
We address the easy ones, but they should probably be all removed.
|
|
in CArray
|
|
The old unification engine was using the unfiltered environment when a
context had been cleared, leading to an ill-typed goal.
|
|
|
|
|
|
|
