| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
- Monomorphize Cst_stack to 'a = constr.
- Add corresponding debug printer.
|
| |
|
|
|
|
|
| |
conclusion, and results of
unifying the lemma with subterms. Using Retyping.get_type_of instead results in 3x
speedup in Ncring_polynom.
|
| |
|
|
| |
by the printing options (i.e. when "Print Universes" is set).
|
| |
|
|
| |
by the printer anyway.
|
| |
|
|
| |
- 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.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
allowing fast conversion to be used during unification while respecting the
semantics of unification w.r.t universes.
- Inside kernel, checked_conv is used mainly, it just does checking, while infer_conv
is used for module subtyping.
- Outside, infer_conv is wrapped in Reductionops to register the right constraints
in an evarmap.
- In univ, add a flag to universes to cache the fact that they are >= Set, the
most common constraints, resulting in an 4x speedup in some cases (e.g. HigmanS).
|
| |
|
|
| |
different places
|
| | |
|
| |
|
|
|
|
| |
polymorphic
constants.
|
| |
|
|
| |
- Finish the change to level-to-level substitutions, in the checker.
|
| |
|
|
|
|
|
| |
- 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.
|
| |
|
|
|
|
|
| |
collapsed universes.
- Fix normalization with universe substitutions during refinement being inconsistent
with the one in the kernel.
|
| |
|
|
|
| |
Of course, this is an under approximation of the expected behavior : unfolding
a constant iff a leaf of its underlying split-tree is reached.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
destruction of schemes in Type such as sumbool.
Added an option "Set Standard Proposition Elimination Names" for
governing this strategy (activated by default).
This provides names supposingly more uniform than before for those who
like to have names automatically generated, at least in the first
phase of the development process of proofs.
Examples:
*** Non dependent case ***
Goal {True}+{False}-> True.
intros [|].
Before:
t : True
============================
True
and
f : False
============================
True
After:
H : True
============================
True
H : False
============================
True
*** Dependent case ***
Goal forall x:{True}+{False}, x=x.
intros [|].
Before:
t : True
============================
left t = left t
f : False
============================
right f = right f
After:
HTrue : True
============================
left HTrue = left HTrue
HFalse : False
============================
right HFalse = right HFalse
|
| | |
|
| |
|
|
|
|
| |
cases of Type (* Prop *) <= Set.
- Do check types of metavariables at the end of apply's unification,
if it failed at the beginning (otherwise universe constraints can be incomplete).
|
| |
|
|
| |
(refolding of cbn is smarter)
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
correctly when comparing stacks.
- Disallow Type i <= Prop/Set constraints, that would otherwise allow
constraints that make a universe lower than Prop.
- Fix stm/lemmas that was pushing constraints to the global context,
it is done depending on the constant/variable polymorphic status now.
- Adapt generalized rewriting in Type code to these fixes.
|
| |
|
|
|
|
| |
the merge).
Obligations are not necessarily opaque.
|
| | |
|
| |
|
|
| |
fixing two opened bugs from HoTT/coq.
|
| |
|
|
|
| |
abstraction has the right type. Fixes bug# 3306.
Add test-suite files for bugs 3305 and 3306.
|
| |
|
|
| |
problem with hashconsing at the same time. This fixes bug# 3302.
|
| | |
|
| |
|
|
|
|
|
| |
#3302) by considering
Type i a ground term even when "i" is a flexible universe variable, using the infer_conv
function to do the unification of universes.
|
| |
|
|
|
|
|
|
| |
evar_map
in tactics, avoiding useless and potentially costly merge's of constraints.
- Implement revert and generalize using the new tactics (not bound to syntax though,
as they are not backwards-compatible yet).
|
| | |
|
| |
|
|
|
|
|
|
|
| |
in the Evd of proofs (Evd.from_env).
- Allow to set the Store.t value of new evars, e.g. to set constraint evars as
unresolvable in rewrite.ml.
- Fix a HUGE performance problem in the processing of constraints, which was remerging
all the previous constraints with the ambient global universes at each new constraint addition.
Performance is now back to (or better than) normal.
|
| |
|
|
|
|
|
| |
eagerly solve l <= k constraints as k := l when k is a fresh variable coming
from a template type. This has the effect of fixing the variable at the first
instantiation of the parameters of template polymorphic inductive and avoiding
to generate useless <= constraints that need to be minimized afterwards.
|
| | |
|
| |
|
|
|
| |
- Fix in canonical structure inferce, we have to check that the heads
are convertible and keep universe information around.
|
| |
|
|
| |
polymorphic (fixes bug #3043).
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
- 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.
|
| | |
|
| |
|
|
|
|
|
|
| |
indeed unifies
with the projected term, keeping track of universes).
- Fix the [unify] tactic to fail properly.
- Fix unification to disallow lowering a global Type(i) universe to Prop or Set.
|
| |
|
|
|
|
| |
- Fix passing of universe contexts through definitions/proofs, abstract is ok now, even
in presence of polymorphism
- Correctly mark unresolvable the evars made by the Simple abstraction.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
universes (better semantics
for axioms, opaque constants).
Conflicts:
pretyping/evarconv.ml
|
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Pierre Boutillier