aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_ltac.ml4
AgeCommit message (Expand)Author
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
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-10-01Added a new tactical infoH tac, that displays the names of hypothesis created...courtieu
2012-08-08Updating headers.herbelin
2012-07-19Getting rid of the undocumented [complete] tactic, which wasppedrot
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-30Restore compatibility with camlp4 (some missing open Tok)letouzey
2012-05-29Migrate the grammar entry about "Ltac" into g_vernac.ml4.letouzey
2012-05-29simplification in deps of some g_*.ml4letouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-03-18A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsletouzey
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 23:51:25 +0000