aboutsummaryrefslogtreecommitdiff
path: root/ltac/g_ltac.ml4
AgeCommit message (Expand)Author
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-28Merge remote-tracking branch 'github/pr/232' into v8.6Maxime Dénès
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-09-15Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Pierre-Marie Pédrot
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-09-14Moving the tactic-in-term extension from G_constr to G_ltac.Pierre-Marie Pédrot
2016-09-11Move Ltac-specific components from G_proofs to G_ltac.Pierre-Marie Pédrot
2016-09-08Making Vernacexpr independent from Tacexpr.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-30Goal selectors now use the keyword [only].Cyprien Mangin
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-17par: like all: but in parallelEnrico Tassi
2016-06-16Typo in comment.Hugo Herbelin
2016-06-16Fixing parsing of constr argument of ltac functions at level 8 in theHugo Herbelin
2016-06-16Merge 'pr/191' into trunkEnrico Tassi
2016-06-14Ident selectors cannot be used inside an Ltac expression.Cyprien Mangin
2016-06-14Goal selectors are now tacticals and can be used as such.Cyprien Mangin
2016-06-14Remove the need for brackets in goal selectors.Cyprien Mangin
2016-06-14Fix usage of Pervasives in goal selectors.Cyprien Mangin
2016-06-14Fix the pretty-printing of goal range selectors.Cyprien Mangin
2016-06-14Add goal range selectors.Cyprien Mangin
2016-06-06STM: proof block detection for par:Enrico Tassi
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
2016-06-05Adding the Print Ltac Signature command.Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-10Removing the Entry module now that rules need not be marshalled.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-04-27Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"Hugo Herbelin
2016-04-27Revert "Typo in comment."Hugo Herbelin
2016-04-27Typo in comment.Hugo Herbelin
2016-04-27Fixing parsing of constr argument of ltac functions at level 8 in theHugo Herbelin
2016-04-24Higher-level API for tactic notations.Pierre-Marie Pédrot
2016-04-14Moving and enhancing the grammar_tactic_prod_item_expr type.Pierre-Marie Pédrot
2016-04-09Removing extra spaces in printing arguments of VERNAC EXTEND.Hugo Herbelin
2016-04-09Re-add printer for tacdef_body so that Ltac definitions are printed by pr_ver...Hugo Herbelin
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 04:04:09 +0000