aboutsummaryrefslogtreecommitdiff
path: root/printing/pptactic.ml
AgeCommit message (Collapse)Author
2014-08-29Type-safe version of genarg list / pair / opt functions.Pierre-Marie Pédrot
2014-08-18Lazy interpretation of patterns so that expressions such as "intros H H'/H"Hugo Herbelin
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.
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
"pat/term" for "apply term on current_hyp as pat".
2014-08-18Reorganisation of intropattern codeHugo Herbelin
- 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?
2014-08-18Refine patch for behavior of unify_to_subterm to allow backtracking onMatthieu Sozeau
unsatisfiable constraint failures but give sensible error messages if an occurrence was found and only typeclass resolution failed. Fixes MathClasses.
2014-08-18Moving the TacAlias node out of atomic tactics.Pierre-Marie Pédrot
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
Also taking advantage of the change to rename it into TacML. Ultimately should allow ML tactic to return values.
2014-08-12A couple of fixes/improvements in -beautify, but backtracking onHugo Herbelin
change of printing format of forall (need more thinking).
2014-08-07Removing simple induction / destruct from the AST.Pierre-Marie Pédrot
2014-08-07Instead of relying on a trick to make the constructor tactic parse, putPierre-Marie Pédrot
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.
2014-08-07Removing the "constructor" tactic from the AST.Pierre-Marie Pédrot
2014-08-06Removing "intros untils" from the AST.Pierre-Marie Pédrot
2014-08-05Fixing a few beautifying bugs.Hugo Herbelin
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
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).
2014-08-05Adding a syntax "enough" for the variant of "assert" with the order ofHugo Herbelin
subgoals and the role of the "by tac" clause swapped.
2014-08-01New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Arnaud Spiwack
Differs from the usual t;[t1…tn] in two ways: * It can be used without a preceding tactic * It counts every focused subgoal, rather than considering independently the goals generated by the application of the preceding tactic on individual goals. In other words t;[t1…tn] is [> t;[>t1…tn].. ].
2014-08-01Add [numgoal] to Ltac.Arnaud Spiwack
2014-08-01Fix typo in cf04daec997.Arnaud Spiwack
2014-07-29Untyped terms in tactic: function [type_term c] to give a typed version of [c].Arnaud Spiwack
2014-07-29Add a type of untyped term to Ltac's value.Arnaud Spiwack
It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218. The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation.
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
potentially conflicting tactics names from different plugins.
2014-07-25Removing dead code relative to or_metaid.Pierre-Marie Pédrot
2014-07-24Distinguish tactics t1;t2 and t1;[t2..].Arnaud Spiwack
They used to be the same (and had a single entry in the AST). But now that t2 can be a multi-goal tactic, t1;[t2..] has the semantics of executing t2 in each goal independently.
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
backtracks, print time spent in each of successive calls.
2014-07-07Revert "time tac" (committed by mistake).Hugo Herbelin
This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
2014-07-07time tacHugo Herbelin
2014-06-06Moving the [split] tactic out of the AST.Pierre-Marie Pédrot
2014-05-22Moving the "specialize" tactic out of the AST. Also removed an obsoletePierre-Marie Pédrot
variant of it, accepting an additional integer.
2014-05-22Removing useless use of metaids in tactic AST.Pierre-Marie Pédrot
2014-05-21Removing decompose record / sum from the tactic AST.Pierre-Marie Pédrot
2014-05-21Moving left & right tactics out of the AST.Pierre-Marie Pédrot
2014-05-20Moving (e)transitivity out of the AST.Pierre-Marie Pédrot
2014-05-20Tentative to add constr-using primitive tactics without grammar rules.Pierre-Marie Pédrot
We eta-expand primitive Ltac functions, and instead of feeding TacExtend directly with its arguments, we use the environment to retrieve them. Some tactics from the AST were also moved away and made using this mechanism.
2014-05-16Moving argument-free tactics out of the AST into a dedicatedPierre-Marie Pédrot
"coretactics.ml4" file.
2014-05-16Slightly better printer for native ML tactics, in order to disambiguatePierre-Marie Pédrot
them.
2014-04-14Closing bug #3260Julien Forest
adding a new grammar entry for clauses
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
The removed code isn't used locally and isn't exported in the signature
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
NB: new file miscprint.ml deserves to be part of printing.cma, but should be part of proofs.cma for the moment, due to use in logic.ml
2013-12-19Removing the useless pattern ident genarg.Pierre-Marie Pédrot
2013-12-19Printing function for Stdargs in debuggerPierre Boutillier
2013-12-01Removing RefArgType generic argument.Pierre-Marie Pédrot
2013-11-30Getting rid of casted_open_constr. It was only used by thePierre-Marie Pédrot
refine tactic, which now uses plain glob_constr's. Now there is no real need to depend on goal when interpreting genargs. Possible minor incompatibilities: 1. The interpretation of glob_constr to constr is now done by Goal.constr_of_raw, which may be slightly dumbier than the dedicated Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite do go through, though. 2. I had to change the parsing level of wit_glob in Extraargs from lconstr to constr. It may break ML notations using glob, but as they are only used inside Coq code and all well-parenthezised, it should be OK.
2013-11-13Synchronizing the printer of tactic notations.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17084 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
Instead of putting the body directly in the AST, we register it in a table. This time it should work properly. Tactic notation are given kernel names to ensure the unicity of their contents. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
Tactics notation interpretation was messed up because of the use of identical keys for different notations. All my tentative fixes were unsuccessful, so better blankly revert the commit for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17078 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
Instead of putting the body directly in the AST, we register it in a table. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17077 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Update comments.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17033 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds an experimental exactly_once tactical.aspiwack
exactly_once t, will have a success if t has exactly once success. There are a few caveats: - The underlying effects of t may happen in an unpredictable order (hence it may be wise to use it only with "pure" tactics) - The second success of a tactic is conditional on the exception thrown. In Ltac it doesn't show, but in the underlying code, the tactical also expects the exception you want to use to produce the second success. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17009 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a tactical once.aspiwack
[once t] does just as [t] but has exactly one success it [t] has at least one success. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17004 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Added the tactical "tac1 + tac2".aspiwack
It works pretty much like "tac1 || tac2" except that it has as successes all the successes of tac1 followed by all the successes of tac2 (whereas the latter has either the successes of tac1 (if there is at least one) or those of tac2 (otherwise)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16998 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 08:40:53 +0000