| Age | Commit message (Collapse) | Author |
|---|
|
|
|
unification, speeding it up considerably
Revert backwards-incompatible commit 77df7b1283940d979d3e14893d151bc544f41410
|
|
which
results in strange changes in user provided terms.
|
|
|
|
|
|
which made CoRN (and probably Ergo) fail. Another option should be found for
making a constant not unfoldable by tactics/refinement.
|
|
converting
the stacks. Take care of this by recalling unification.
|
|
from MathClasses).
|
|
kernel in library/universes.ml.
|
|
cleanly when called
on partially applied constructors. Also protect evar_conv from that case.
|
|
of the universe context in the obligations, it gets gradually fixed
globally by each one of them.
Fixes bug found in Misc/Overloading.
|
|
invariant that the evar arguments to that function always have to be undefined.
|
|
|
|
|
|
variable
as algebraic so it can disappear from the proof (it always gets substituted away from
the term). This means less spurious universes remaining in proof terms.
|
|
reductions in
case the constant was hiding a direct match for example. Also avoid two lookups
of ReductionBehavior per constant application in simpl.
|
|
|
|
a global reference that the current (goal) env contains all the
section variables that the global reference expects to be present.
Note that the test for inclusion might be costly: everytime a
conversion happens in a section variable copied in a goal, this
conversion has to be redone when referring to a constant dependent on
this section variable.
It is unclear to me whether we should not instead give global names to
section variables so that they exist even if they are not listed in
the context of the current goal.
Here are two examples which are still problematic:
Section A.
Let B := True : Type.
Definition C := eq_refl : B = True.
Theorem D : Type.
clearbody B.
set (x := C).
unfold C in x.
(* inconsistent context *)
or
Section A.
Let B : Type.
exact True.
Qed.
Definition C := eq_refl : B = True. (* Note that this violated the Qed. *)
Theorem D : Type.
set (x := C).
unfold C in x.
(* inconsistent context *)
|
|
into a specific new cleaned file find_subterm.ml.
This makes things clearer but also solves some dependencies problem
between Evd, Termops and Pretype_errors.
|
|
not a variable, in the future objective to factorize code between
"generalize dependent" and "set", "destruct", etc.
|
|
proof engine. Moved it to unification.ml.
|
|
|
|
form of a potential canonical argument anymore, and we check that it may be part
of a canonical structure first.
|
|
incompatibilities, at least until the check of compilation of contribs
succeeds more often.
Incidentally adapted some proofs in Reals which were not agnostic
relatively to whether the option is on or off.
|
|
is has non-local effects. For now it is not disabled by default, but we'll
try to disable it once the test-suite and contribs are stabilized.
|
|
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.
|
