aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Protect against "it's unifiable, if you solve some unsolvable constraints" ↵Gravatar Matthieu Sozeau2014-08-27
| | | | | | | | 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.
* Removing spurious tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-27
| | | | | | 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.
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
| | | | | to match on a primitive projection application c.(p) using "?f _", binding f to (fun x => x.(p)) with the correct typing.
* Add an is_cofix tacticGravatar Jason Gross2014-08-25
| | | | | | 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?
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
|
* Fixing previous commit.Gravatar Pierre-Marie Pédrot2014-08-25
|
* Fixing a bug introduced in the extension of 'apply in' + simplifying code.Gravatar Hugo Herbelin2014-08-25
|
* Tactics.is_quantified_hypothesis does not reduce anymore to decide whetherGravatar Pierre-Marie Pédrot2014-08-23
| | | | | 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.
* Tactics.unify in the new monad.Gravatar Pierre-Marie Pédrot2014-08-23
|
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
|
* Removing unused parts of the Goal.sensitive monad.Gravatar Pierre-Marie Pédrot2014-08-21
| | | | | | 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.
* Removing a Goal.sensitive in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
|
* Removing a use of tclSENSITIVE in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
|
* Removing a use of tclSENSITIVE in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
|
* Removing a use of tclSENSITIVE in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
|
* Removing a use of Goal.refine.Gravatar Pierre-Marie Pédrot2014-08-19
|
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
| | | | | | | 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.
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
| | | | "pat/term" for "apply term on current_hyp as pat".
* Improving error message when applying rewrite to an expression which is not ↵Gravatar Hugo Herbelin2014-08-18
| | | | an equality.
* Factorizing cutrewrite (to be made obsolote) and dependent rewrite (toGravatar Hugo Herbelin2014-08-18
| | | | | | | | | | | 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).
* A few more comments in tactics.mli and hippatern.ml.Gravatar Hugo Herbelin2014-08-18
|
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
| | | | Isolating a core tactic in replace, shareable to cutrewrite.
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
| | | | | scheme, redundancies, possibility of chaining a tactic knowing the name of introduced hypothesis, new proof engine).
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
| | | | | | | | | | | | | | | | - 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?
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
| | | | | | | | | - 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)
* Refine patch for behavior of unify_to_subterm to allow backtracking onGravatar Matthieu Sozeau2014-08-18
| | | | | | unsatisfiable constraint failures but give sensible error messages if an occurrence was found and only typeclass resolution failed. Fixes MathClasses.
* Moving the TacAlias node out of atomic tactics.Gravatar Pierre-Marie Pédrot2014-08-18
|
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
| | | | | Also taking advantage of the change to rename it into TacML. Ultimately should allow ML tactic to return values.
* Better printing of Ltac values.Gravatar Pierre-Marie Pédrot2014-08-16
|
* Fixing too restrictive detection of resolution of evars in "apply in"Gravatar Hugo Herbelin2014-08-16
| | | | (revealed by contribution PTSF).
* More self-contained code for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
|
* Removing unused Refiner.tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
|
* Remove confusing behavior of unify_with_subterm that could fail withGravatar Matthieu Sozeau2014-08-14
| | | | | | | NoOccurenceFound when only typeclass resolution failed. Might break some scripts relying on backtracking on typeclass resolution failures to find other terms to rewrite, which can be fixed using occurrences or directly setoid_rewrite.
* Restore the error-handling behavior of [change], which was silently failingGravatar Matthieu Sozeau2014-08-14
| | | | when conversion in the goal failed.
* Fix elimschemes accessing directly the universe context of inductives (fixes ↵Gravatar Matthieu Sozeau2014-08-14
| | | | | | test-suite file HoTT_coq_089.v).
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
|
* In Hipattern: some functions not working modulo evar instantiation.Gravatar Arnaud Spiwack2014-08-07
| | | In theory [Proofview.Goal.env] should be, itself, marked as requiring a normalised goals (as it includes [hyps] which does). However, it is impractical as it is very common to pass a goal environment to a function reasoning modulo evars. So I guess we are bound to mark the appropriate functions by hand.
* Removing simple induction / destruct from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
|
* Instead of relying on a trick to make the constructor tactic parse, putGravatar Pierre-Marie Pédrot2014-08-07
| | | | | | | | | | all the tactics using the constructor keyword in one entry. This has the side-effect to also remove the other variant of constructor from the AST. I also needed to hack around the "tauto" tactic to make it work, by calling directly the ML tactic through a TacExtend node. This may be generalized to get rid of the intermingled dependencies between this tactic and the infamous Ltac quotation mechanism.
* Removing the "constructor" tactic from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
|
* Revert the change in Constrintern introduced by "Add a type of untyped term ↵Gravatar Arnaud Spiwack2014-08-06
| | | | | | | to Ltac's value." It was commit 52247f50fa9aed83cc4a9a714b6b8f779479fd9b. The closure in uconstr renders these changes (pertaining to substitution of ltac variables during internalisation) obsolete.
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
| | | | | This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine. As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile.
* Removing "intros untils" from the AST.Gravatar Pierre-Marie Pédrot2014-08-06
|
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
| | | | | | | | | | hypothesis when using it in apply or rewrite (prefix ">", undocumented), and a modifier to explicitly keep it in induction or destruct (prefix "!", reminiscent of non-linerarity). Also added undocumented option "Set Default Clearing Used Hypotheses" which makes apply and rewrite default to erasing the hypothesis they use (if ever their argument is indeed an hypothesis of the context).
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
| | | | subgoals and the role of the "by tac" clause swapped.
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
| | | | | | | | | | | | | 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.
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
| | | | | par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
* Ltac's [idtac] is now interpreted outside of a goal if possible.Gravatar Arnaud Spiwack2014-08-05
| | | | It avoids printing several times the same things when no constr are involved in the message. It also allows to print messages even after all goals have been solved.
* Ltac's idtac is now implemented using the new API.Gravatar Arnaud Spiwack2014-08-05
|
* Tacinterp: [interp_message] and associate now only require an environment ↵Gravatar Arnaud Spiwack2014-08-05
| | | | rather than an entire goal.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 08:35:34 +0000