| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
structure.
|
| |
|
|
| |
Add a flag to disallow minimization to set
|
| |
|
|
|
|
| |
According to their polymorphic/non-polymorphic status, which
imply that universe variables introduced with it are assumed
to be >= or > Set respectively in the following definitions.
|
| | |
|
| |
|
|
|
| |
We are forced to declare universes that are global and appear in the
local constraints as we start from an empty universe graph.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.
2) Do not remove non-recursive variables when computing minimal levels of inductives.
3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.
4) We correctly solve the recursive equations taking into account the
user-declared level.
|
| |
|
|
| |
Wrong handling of algebraic universes that have upper bounds.
|
| |
|
|
|
|
| |
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
|
| |
|
|
|
| |
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
|
| |
|
|
| |
has a strict upper bound.
|
| |
|
|
| |
[compare_head_gen] defined in terms of [compare_head_gen_leq]. Remove an unused argument from [compare_head_gen_leq].
|
| |
|
|
| |
printing functions touched in the kernel).
|
| | |
|
| |
|
|
|
|
|
| |
inductive types (i.e., ones declared with an explicit anonymous Type
at the conclusion of their arity). With this change one can force
inductives to live in higher universes even in the non-fully universe
polymorphic case (e.g. bug #3821).
|
| |
|
|
| |
This is a continuation of the previous patch.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
|
| |
|
|
|
|
|
|
| |
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
|
| |
|
|
| |
projections with their eta-expanded constant form.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
variables.
Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.
|
| | |
|
| |
|
|
|
| |
and disable hashconsing of substituted instances which had a huge performance
penalty in general. They are hashconsed when put in the environment only now.
|
| |
|
|
| |
kernel in library/universes.ml.
|
| | |
|
| |
|
|
| |
universe instance.
|
| |
|
|
|
|
| |
and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.
|
| | |
|
| |
|
|
| |
- More cleanup. remove unneeded functions in universes
|
| |
|
|
|
|
|
|
| |
Universes.
Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
|
| | |
|
| |
|
|
|
|
|
| |
- Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}.
These are always rigid.
- Use level-to-level substitutions where the more general level-to-universe substitutions
were previously used.
|
| |
|
|
|
| |
Fix restriction of universe contexts to not forget about potentially useful
constraints.
|
| |
|
|
| |
minimization.
|
| |
|
|
|
| |
- Fix in canonical structure inferce, we have to check that the heads
are convertible and keep universe information around.
|
| |
|
|
|
|
| |
- Enforce that no u <= Prop/Set can be added for u introduced by the user in Evd.process_constraints.
(Needs to be enforced in the kernel as well, but that's the main entry point).
- Fix a test-suite script and remove a regression comment, it's just as before now.
|
| |
|
|
| |
term.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Remove Universe Polymorphism flags everywhere.
- Properly infer, discharge template arities and fix substitution inside them
(kernel code to check for correctness).
- Fix tactics that were supposing universe polymorphic constants/inductives to
be parametric on that status. Required to make interp_constr* return the whole evar
universe context now.
- Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing,
sadly losing most of its benefits.
Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting
all serialization code.
Conflicts:
kernel/univ.ml
tactics/tactics.ml
theories/Logic/EqdepFacts.v
|
| | |
|
| |
|
|
|
|
|
|
|
| |
constraints,
and keeping spurious equalities. simplify_universe_context is correct, although
it might keep unused universes around (it's the responsibility of the tactics to
not produce unused universes then).
Add printer for future universe contexts for debugging.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
- Avoid generation of dummy universes for unsafe_global*
- Handle side effects better for polymorphic definitions.
Conflicts:
kernel/term_typing.ml
tactics/tactics.ml
|
| |
|
|
|
|
| |
- Shortcut for Set <= x checks, assuming that this is always true except when
x (or rather its canonical representative) is Prop. Invariant to check.
- Uncomment the profiling code and make it depend on a (statically known) boolean.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
A try at hashconsing all universes instances seems to incur a big cost.
- Do hashconsing of universe instances in constr.
- Little fix in obligations w.r.t. non-polymorphic constants.
Conflicts:
kernel/constr.ml
kernel/declareops.ml
kernel/inductive.ml
kernel/univ.mli
|
| |
|
|
| |
stdlib does not compile entirely).
|
Matthieu Sozeau
Arnaud Spiwack
Matthieu Sozeau
Maxime Dénès
Pierre-Marie Pédrot
Enrico Tassi
Jason Gross