| Age | Commit message (Collapse) | Author |
|---|
|
|
|
cleaning done in e8c47b652a0.
It had no serious consequences except having whd-reduction blocked on
a let-in when typing a return clause with let-ins in the arity (a
priori resulting in return types of the form e.g. "(let x:=t in fun y
=> T) u" instead of T[x:=t;y:=u], if I'm not mistaking).
This fixes 3210.v in test-suite.
|
|
|
|
|
|
|
|
same evar.
|
|
- prod_applist
- prod_applist_assum
- lambda_applist
- lambda_applist_assum
expect an instance matching the quantified context. They are now in
term.ml, with "list" being possibly "vect".
Names are a bit arbitrary. Better propositions are welcome. They are
put in term.ml in that reduction is after all not needed, because the
intent is not to do β or ι on the fly but rather to substitute a λΓ.c
or ∀Γ.c (seen as internalization of a Γ⊢c) into one step,
independently of the idea of reducing.
On the other side:
- beta_applist
- beta_appvect
are seen as optimizations of application doing reduction on the fly
only if possible. They are then kept as functions relevant for
reduction.ml.
|
|
It will later be used to fix a bug and improve some code.
Interestingly, there were a redundant semantic equivalent to
extended_rel_list in the kernel called local_rels, and another private
copy of extended_rel_list in exactly the same file.
|
|
|
|
Redefining adjust_subst_to_rel_context from instantiate_context who
was hidden in inductiveops.ml, renamed the latter into
subst_of_rel_context_instance and moving them to Vars. The new name
highlights that the input is an instance (as for applist) and the
output a substitution (as for substl). This is a clearer unified
interface, centralizing the difficult de-Bruijn job in one place. It
saves a couple of List.rev.
|
|
cleaning the interfaces is eventually easier. Here, adding
find_mrectype_vect to simplify vnorm.ml.
|
|
|
|
|
|
projections (off by default).
|
|
|
|
Prop levels.
As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
|
|
Instead of accumulating constraints which are not present in the original
graph, we parametrize the equality function by a function actually merging
those constraints in the current graph. This prevents doing the work twice.
|
|
|
|
This was not a typo (was correctly taking the family type of the type).
|
|
|
|
parameters of an inductive type.
|
|
|
|
Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in
8.5beta2 and 8.5beta3 from a Coq file because typing done while
compiling "match" would serve as a protection. However exploitable by
calling the kernel directly, e.g. from a plugin (but a plugin can
anyway do what it wants by bypassing kernel type abstraction).
Fixing similar error in pretyping.
|
|
|
|
constr, and the associated signature, not needed anymore.
Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
|
|
The clenv_fchain function was needlessly merging universes coming from
two evarmaps even though one was an extension of the other. A flag was
added so that the tactic just retrieves the newer universes.
|
|
|
|
unification (not necessarily preserved due to the fo approximation rule).
|
|
only one disjoint component of the typeclasses instances to resolve.
|
|
their type annotation.
|
|
This reverts commit 07620386b3c1b535ee7e43306a6345f015a318f0.
Very sorry not ready.
|
|
the return clause and of the branches in a "match", computing them
automatically when using the "at" clause of pattern, destruct, ...
In principle, this is a source of incompatibilities in the numbering,
since the internal binders of a "match" are now skipped. We shall deal
with that later on.
|
|
Did some manual merge in tactics/tactics.ml.
|
|
|
|
this type is a proposition. This is based on the assumption that in
Prop, what matters first is the statement.
|
|
|
|
whd_evar in refresh_universes.
|
|
|
|
When refreshing a type variable, always use a rigid universe to force the most
general universe constraint, as in 8.4.
|
|
|
|
make them rigid to disallow minimization.
|
|
universes are declared correctly in the enclosing proofs evar_map's.
|
|
|
|
|
|
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
|
|
Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing. When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined. Only when the
comparison is successful the private_constant is not re-checked. Otherwise
else it is. In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.
Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron). Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.
|
|
Universe instances for constructors were not always correct, for instance in:
[cons _ list (nil _)] with a polymorphic [list] type, [nil] was receiving an
empty instance.
|
|
- Universes are now represented in the VM by a structured constant containing the
global levels. This constant is applied to local level variables if any.
- When reading back a universe, we perform the union of these levels and return
a [Vsort].
- Fixed a bug: structured constants could contain local universe variables in
constructor arguments, which has to be prevented.
Was showing up for instance when evaluating [cons _ list (nil _)] with
a polymorphic [list] type.
- Fixed a bug: polymorphic inductive types can have an empty stack.
Was showing up when evaluating [bool] with a polymorphic [bool] type.
- Made a few cosmetic changes.
Patch written with Benjamin Grégoire.
|
|
Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with
a polymorphic prod.
|
|
polymorphic definitions.
- This implementation passes universes in separate arguments and does not
eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
|
