| Age | Commit message (Collapse) | Author |
|---|
|
This reverts commit 5b92ff7b0a641bf2daa31b60bf49b57a5d1e8452.
|
|
This reverts commit afa441019432f70245fed6adc5eb0318514e4357.
|
|
Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
|
|
This should allow tactics after a Goal.enter not to have to renormalize
them uselessly.
|
|
|
|
Local Ltac definitions do not register their name in the nametab anymore,
thus elegantly solving the bug. The tactic body remains accessible from
the tactic engine, but the name is rendered meaningless to the userside.
|
|
|
|
|
|
|
|
fresh names interferring with names later generated in intropatterns
(as introduced in 72498d6d68ac which passed "clenv_refine_in continued
by pattern introduction" to descend_in_conjunction while only a pure
clenv_refine was passed before). The 72498d6d68ac version was
generating fresh names in the wrong order (morally-private names for
descend_in_conjunction before user-level names in clenv_refine_in).
The 19a7a5789c fix was introducing expressions not handled by the
refine from logic.ml.
In particular, this fixes RelationAlgebra.
|
|
|
|
|
|
|
|
ML tactics that may be used as simple identifiers are now declared as
a true Ltac entry pertaining to the module that contains the Declare ML
Module statement.
|
|
This allows to directly register globtactics in the Tacenv API, without
having to resort to any internalization function.
|
|
|
|
Instead of having a version of unpackers for each level, we use a dummy argument
to force unification of types.
|
|
at least remove the successes obtained by trivial unification of a
meta with the goal, so as to avoid surprising results. We generalize
this to variables which will only eventually be replaced by metas.
|
|
|
|
behavior of evar_conv_x,
getting more common after patch on evars and eta. The main problem is that ?X = C[?X] problems get
postponed now, when they failed earlier before (rendering the algorithm incomplete, e.g. on ?X = \y. ?X y).
A notion of "rigid/strongly rigid" occurrences would give a better fix.
|
|
Indeed [tclWITHHOLES false tac sigma x] is equivalent to [tclEVARS sigma <*> tac x]
and we should try to reduce the use of this tactical, because it is mostly
a legacy tactic.
|
|
to match on a primitive projection application c.(p) using "?f _", binding f
to (fun x => x.(p)) with the correct typing.
|
|
Should we also add is_* tactics for other things? is_rel, is_meta,
is_sort, is_cast, is_prod, is_lambda, is_letin, is_app, is_const,
is_ind, is_constructor, is_case, is_proj?
|
|
|
|
|
|
|
|
a variable is quantified in the goal. This is only used by induction, and
it should be a bad practice to depend on an invisible binder.
|
|
|
|
|
|
Some legacy code remains to keep the newish refine tactic working, but
ultimately it should be removed. I did not manage to do it properly though,
i.e. without breaking the test-suite furthermore.
|
|
|
|
|
|
|
|
|
|
|
|
can be given with second H bound by the first one.
Not very satisfied by passing closure to tactics.ml, but otherwise
tactics would have to be aware of glob_constr.
|
|
"pat/term" for "apply term on current_hyp as pat".
|
|
an equality.
|
|
integrate to "rewrite"?) with the code of "replace".
Incidentally, "inversion" relies on dependent rewrite, with an
incompatibility introduced. Left-to-right rewriting is now done with
"eq_rec_r" while before it was done using "eq_rec" of "eq_sym". The
first one reduces to the second one but simpl is not anymore able to
reduce "eq_rec_r eq_refl". Hopefully cbn is able to do it (see
Zdigits).
|
|
|
|
Isolating a core tactic in replace, shareable to cutrewrite.
|
|
scheme, redundancies, possibility of chaining a tactic knowing the
name of introduced hypothesis, new proof engine).
|
|
- emphasizing the different kinds of patterns
- factorizing code of the non-naming intro-patterns
Still some questions:
- Should -> and <- apply to hypotheses or not (currently they apply to
hypotheses either when used in assert-style tactics or apply in, or
when the term to rewrite is a variable, in which case "subst" is
applied)?
- Should "subst" be used when the -> or <- rewrites an equation x=t
posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)?
- Should -> and <- be applicable in non assert-style if the lemma has
quantifications?
|
|
- made "apply" tactics of type Proofview.tactic, as well as other inner
functions about elim and assert
- used same hypothesis naming policy for intros and internal_cut (towards a
reorganization of intro patterns)
- "apply ... in H as pat" now supports any kind of introduction
pattern (doc not changed)
|
|
unsatisfiable constraint failures but give sensible error messages if
an occurrence was found and only typeclass resolution failed.
Fixes MathClasses.
|
|
|
|
Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
|
|
|
|
(revealed by contribution PTSF).
|
|
|
