| Age | Commit message (Collapse) | Author |
|---|
|
the computed direction argument. In case pbty is conv, no refreshing is done
as the evar body must be convertible with the given term, however refreshing
of template application evar arguments can still happen.
(Re)-Closing bug #2966.
|
|
|
|
univ_depends.
Also add a missing constraint when generating a fresh universe for a template polymorphic
inductive in that case.
|
|
matching
infered predicate, instead of the arguments ts which might be empty (e.g. in unification).
Fixes failure in success/unification.v
|
|
Fixes FingerTree contrib.
|
|
for building polymorphic instances of template polymorphic inductives.
|
|
there is not the same as in Evd.define.
- Fixed bugs #3330 and #3331.
|
|
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)
|
|
|
|
|
|
|
