aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_ltac.ml4
Commit message (Collapse)AuthorAge
* Moving Tacinterp to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
|
* Fixing compilation with old versions of CAMLP5.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Moving the parsing of the Ltac proof mode to G_ltac.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].Gravatar Pierre-Marie Pédrot2016-03-04
|
* Exchanging roles of tactic_arg and tactic_top_or_arg entries.Gravatar Pierre-Marie Pédrot2016-03-04
| | | | | | The tactic_arg entry was essentially a hack to keep parsing constrs as tactic arguments. We rather use tactic_top_or_arg as the true entry for tactic arguments now.
* Removing the UConstr entry of the tactic_arg AST.Gravatar Pierre-Marie Pédrot2016-03-04
| | | | | This was redundant with the wit_uconstr generic argument, so there was no real point on keeping it there.
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
|
* Uniformizing the parsing of argument scopes in Ltac.Gravatar Pierre-Marie Pédrot2016-03-04
|
* Removing the MetaIdArg entry of tactic expressions.Gravatar Pierre-Marie Pédrot2016-02-24
| | | | | | This was historically used together with the <:tactic< ... >> quotation to insert foreign code as $foo, but it actually only survived in the implementation of Tauto. With the removal of the quotation feature, this is now totally obsolete.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Partial backtrack on commit 20641795624.Gravatar Pierre-Marie Pédrot2015-12-23
| | | | | | | | | | | | The parsing rules were broken and disallowed tactic replacement of the form Ltac ident ::= expr.
* | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
|/ | | | | | | | | | The definition of Vernacexpr.VernacDeclareTacticDefinition was changed. The original definition allowed us to represent non-sensical value such as: VernacDeclareTacticDefinition(Qualid ..., false, ...) The new definition prevents that.
* Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
|
* grammar: export constr_evalGravatar Enrico Tassi2015-03-30
|
* Fixed 3233 (fresh does not work with a qualid).Gravatar Pierre Courtieu2015-02-23
| | | | | | fresh now accepts a qualid, and behaves as if given the short name. Since fresh used to accept an id, supporting qualid is IMO not a new feature but just a fix. Hence the fix in v8.5.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* A global [gfail] tactic which works like [fail] except that it fails even if ↵Gravatar Arnaud Spiwack2014-12-23
| | | | | | there is no focused goal. The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
| | | | | | This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select". Fixes #3877.
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19
| | | | [multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
| | | | [tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
| | | | | | | | will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise.
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
| | | | | Left a README, just in case someone will discover the remnants of it decades from now.
* Removing a unused legacy parsing rule.Gravatar Pierre-Marie Pédrot2014-08-24
|
* 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.
* Small refactoring: use [uconstr] instead of [constr] when relevant in ↵Gravatar Arnaud Spiwack2014-08-05
| | | | grammar rules.
* New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Gravatar Arnaud Spiwack2014-08-01
| | | | | | | 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].. ].
* Add [numgoal] to Ltac.Gravatar Arnaud Spiwack2014-08-01
|
* Small refactoring in Ltac parsing rules.Gravatar Arnaud Spiwack2014-07-29
|
* Allow [uconstr:c] as argument of a tactic.Gravatar Arnaud Spiwack2014-07-29
|
* Untyped terms in tactic: function [type_term c] to give a typed version of [c].Gravatar Arnaud Spiwack2014-07-29
|
* Untyped term in tactics: add an grammar entry to construct them.Gravatar Arnaud Spiwack2014-07-29
| | | | The syntax is uconstr:term.
* Distinguish tactics t1;t2 and t1;[t2..].Gravatar Arnaud Spiwack2014-07-24
| | | 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.
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
| | | | backtracks, print time spent in each of successive calls.
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
| | | | This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
* time tacGravatar Hugo Herbelin2014-07-07
|
* Removing useless use of metaids in tactic AST.Gravatar Pierre-Marie Pédrot2014-05-22
|
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
| | | | parsing is plugged.
* Adds an experimental exactly_once tactical.Gravatar aspiwack2013-11-02
| | | | | | | | | | 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
* Adds a tactical once.Gravatar aspiwack2013-11-02
| | | | | | [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
* Added the tactical "tac1 + tac2".Gravatar aspiwack2013-11-02
| | | | | | 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
* Getting rid of IntroPatternArgType.Gravatar ppedrot2013-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16610 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless tactic arguments, and using generic argumentsGravatar ppedrot2013-06-27
| | | | | | instead (proof of concept, to be extended). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16609 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "parse "of" as KEYID "of""Gravatar gareuselesinge2013-06-21
| | | | | | This reverts commit edb2c43e152d40001616485fcf7fdde5d947f7a2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16598 85f007b7-540e-0410-9357-904b9bb8a0f7
* parse "of" as KEYID "of"Gravatar gareuselesinge2013-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Setting "appcontext" as the default behaviour in Ltac matching.Gravatar ppedrot2013-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16537 85f007b7-540e-0410-9357-904b9bb8a0f7
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
| | | | | | | | | | | | | native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
| | | | | | | | | | | | kernel on CAMLP4/5 structures, and consequently should also erase such structures from vo files. This modification requires some code duplication, mainly while reimplementing our own location data type. This is chiefly visible in the ml4 files, where CAMLP4/5 locations must be manually converted to our locations with an explicit (!@) cast operator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 11:16:27 +0000