aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_ltac.ml4
AgeCommit message (Expand)Author
2016-03-20Moving Tacinterp to Hightactics.Pierre-Marie Pédrot
2016-03-19Fixing compilation with old versions of CAMLP5.Pierre-Marie Pédrot
2016-03-19Moving VernacSolve to an EXTEND-based definition.Pierre-Marie Pédrot
2016-03-19Moving the parsing of the Ltac proof mode to G_ltac.Pierre-Marie Pédrot
2016-03-04Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].Pierre-Marie Pédrot
2016-03-04Exchanging roles of tactic_arg and tactic_top_or_arg entries.Pierre-Marie Pédrot
2016-03-04Removing the UConstr entry of the tactic_arg AST.Pierre-Marie Pédrot
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-03-04Uniformizing the parsing of argument scopes in Ltac.Pierre-Marie Pédrot
2016-02-24Removing the MetaIdArg entry of tactic expressions.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-23Partial backtrack on commit 20641795624.Pierre-Marie Pédrot
2015-12-18CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionMatej Kosik
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-03-30grammar: export constr_evalEnrico Tassi
2015-02-23Fixed 3233 (fresh does not work with a qualid).Pierre Courtieu
2015-01-12Update headers.Maxime Dénès
2014-12-23A global [gfail] tactic which works like [fail] except that it fails even if ...Arnaud Spiwack
2014-12-23Fix compilation error in some configurations.Arnaud Spiwack
2014-12-19Add a backtracking version of Ltac's [match].Arnaud Spiwack
2014-12-12Add Ltac syntax for the [tclIFCATCH] primitive.Arnaud Spiwack
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
2014-08-24Removing a unused legacy parsing rule.Pierre-Marie Pédrot
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-08-05Small refactoring: use [uconstr] instead of [constr] when relevant in grammar...Arnaud Spiwack
2014-08-01New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Arnaud Spiwack
2014-08-01Add [numgoal] to Ltac.Arnaud Spiwack
2014-07-29Small refactoring in Ltac parsing rules.Arnaud Spiwack
2014-07-29Allow [uconstr:c] as argument of a tactic.Arnaud Spiwack
2014-07-29Untyped terms in tactic: function [type_term c] to give a typed version of [c].Arnaud Spiwack
2014-07-29Untyped term in tactics: add an grammar entry to construct them.Arnaud Spiwack
2014-07-24Distinguish tactics t1;t2 and t1;[t2..].Arnaud Spiwack
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-07-07Revert "time tac" (committed by mistake).Hugo Herbelin
2014-07-07time tacHugo Herbelin
2014-05-22Removing useless use of metaids in tactic AST.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-11-02Adds an experimental exactly_once tactical.aspiwack
2013-11-02Adds a tactical once.aspiwack
2013-11-02Added the tactical "tac1 + tac2".aspiwack
2013-06-27Getting rid of IntroPatternArgType.ppedrot
2013-06-27Removing useless tactic arguments, and using generic argumentsppedrot
2013-06-21Revert "parse "of" as KEYID "of""gareuselesinge
2013-06-19parse "of" as KEYID "of"gareuselesinge
2013-05-28Setting "appcontext" as the default behaviour in Ltac matching.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:20:56 +0000