| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
After all, let's target 8.6.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
Update the evar_source of the solution evar in evar/evar problems to
propagate the information that it does not necessarily have to be solved
in Program mode.
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
variables of the context of an evar in debugging mode.
|
| | |
| |
| |
| |
| |
| |
| | |
of the return clause and of the branches (what assumed that the
implementation preserves the invariant that the return predicate and
the branches are in canonical [fun Δ => t] form, with Δ possibly
containing let-ins).
|
| | |
| |
| |
| |
| |
| |
| |
| | |
dealing with "match".
Contrastingly, "fix" is considered not to count let-ins for finding
the recursive argument (which is ok because the last argument is
necessarily a lambda).
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
Using the same hack as in the kernel: VM conversion is a reference to
a function, updated when modules using C code are actually linked.
This hack should one day go away, but always linking C code may produce some
other trouble (with the OCaml debugger for instance), so better be safe
for now.
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
math-classes.
|
| | |
| |
| |
| |
| |
| | |
Collecting the bound variables is now done on the glob_constr, before
interpretation, so that only variables given explicitly by the user
are used for binding bound variables.
|
| | |
| |
| |
| |
| |
| |
| | |
which was broken after it became possible to have binding names
themselves bound to ltac variables (2fcc458af16b).
Interpretation was corrected, but error message was damaged.
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
Add a flag to disallow minimization to set
|
| | |
| |
| |
| |
| | |
Retypecheck abstracted infered predicate to register the right
universe constraints.
|
| | |
| |
| |
| |
| | |
Let merge_context_set be lenient when merging the context of side
effects of an entry from solve_by_tac.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
|
| | |
| |
| |
| |
| | |
1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
|
| |\| |
|
| | |
| |
| |
| | |
universe graph
|
| | | |
|
| |\| |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
Pierre-Marie Pédrot
Matthieu Sozeau
Enrico Tassi
Maxime Dénès
Gregory Malecha
Hugo Herbelin
Matthieu Sozeau
Guillaume Melquiond