| Age | Commit message (Collapse) | Author |
|---|
|
universe instance.
|
|
for helping fixing this).
Now the issue is handled solely through refreshing of the terms assigned
to evars during unification.
If ?X = list ?Y, then Y's type is refreshed so that it doesn't mention
a template universe and in turn, ?X won't. Same goes when typechecking
(nil ?X, nil ?Y), the pair constructor levels will be set higher than fresh
universes for the lists carriers. This also handles user-defined functions
on template polymorphic inductives, which was fragile before.
Pretyping and Evd are now uncluttered from template-specific code.
|
|
in Ssreflect).
- Fix is_applied_rewrite_relation to look for propositional relations.
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
applications earlier.
|
|
- Fix HoTT coq bug #80, implicit arguments with primitive projections were
wrongly automatically infered.
|
|
|
|
it was failing with Not_found before previous commit). This "fixes"
the loop by expanding local defs in "imitate" rather than keeping them
explicit. The example is otherwise too large for me to be able to
understand where does the loop come from.
|
|
fix the type of the term which has to be in the signature of the evar
to declare); some problems remain though (see next commit).
|
|
- Remove dead code in evarconv.
|
|
bindings of the same variable (fixing HoTT bug #52). Document the unification
of universes in Ltac/tactics.
|
|
of an anomaly in case
a universe inconsistency occurs when applying a coercion. The statement of the test-suite file
cannot check as is, but does check when the correct FunctorCategory is given, instantiating the TypeCat
to Set.
|
|
name of replaced hypothesis.
|
|
in case prefix 'e' of "apply" and co is not given.
|
|
|
|
primitive projections obey the Arguments command.
|
|
- 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.
|
