| Age | Commit message (Collapse) | Author |
|---|
|
obtained from case analysis or induction. Made it under experimental status.
This replaces commit bf7d2a3ad2535e7d57db79c17c81aaf67d956965 which was
acting at the level of logic.ml. Now acting in tactics.ml.
Parts of things to be done about naming (not related to Propositions):
induction on H:nat+bool produces hypotheses n and b but destruct on H
produces a and b. This is because induction takes the dependent scheme
whose names are statically inferred to be a and b while destruct
dynamically builds a new scheme.
|
|
- Decomment code in reductionops forgotten after debugging.
|
|
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.
|
|
- Allow apply's unification to use conversion even if some polymorphic
constants appear in the goal (consistent with occur_meta_or_evar, and
evarconv in general).
|
|
|
|
- realargs: refers either to the indices of an inductive, or to the proper args
of a constructor
- params: refers to parameters (which are common to inductive and constructors)
- allargs = params + realargs
- realdecls: refers to the defining context of indices or proper args
of a constructor (it includes letins)
- paramdecls: refers to the defining context of params (it includes letins)
- alldecls = paramdecls + realdecls
|
|
catched otherwise due to the discrepancy between evars and metas.
|
|
|
|
Specifications indicating that the record object must be a constructor. Fixes bug #3432.
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
