aboutsummaryrefslogtreecommitdiff
path: root/grammar
AgeCommit message (Expand)Author
2016-02-24Removing the METAIDENT token, as it is not used anymore.Pierre-Marie Pédrot
2016-02-24Removing the Q_coqast module.Pierre-Marie Pédrot
2016-02-01Infering atomic ML entries from their grammar.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-17ML extensions use untyped representation of user entries.Pierre-Marie Pédrot
2016-01-16Tactic notation printing accesses all the token data.Pierre-Marie Pédrot
2016-01-14Removing constr generic argument.Pierre-Marie Pédrot
2016-01-14Removing ident and var generic arguments.Pierre-Marie Pédrot
2016-01-08Monotonizing Ftactic.Pierre-Marie Pédrot
2016-01-06Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-05Fix order of files in mllib.Maxime Dénès
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
2016-01-02Proper datatype for EXTEND syntax tokens.Pierre-Marie Pédrot
2015-12-28Implementing non-focussed generic arguments.Pierre-Marie Pédrot
2015-12-28Removing the special status of open_constr generic argument.Pierre-Marie Pédrot
2015-12-25Fixing non exhaustive pattern-matching in 003fe3d5e60b.Hugo Herbelin
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2015-12-21ARGUMENT EXTEND shares the toplevel representation when possible.Pierre-Marie Pédrot
2015-12-21Removing ad-hoc interpretation rules for tactic notations and their genarg.Pierre-Marie Pédrot
2015-12-21Removing the now useless genarg generic argument.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-17Getting rid of some hardwired generic arguments.Pierre-Marie Pédrot
2015-12-05Factorizing unsafe code by relying on the new Dyn module.Pierre-Marie Pédrot
2015-10-28Type-safe Argextend.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.grammar_prod_item.Pierre-Marie Pédrot
2015-10-27Finer type for Pcoq.interp_entry_name.Pierre-Marie Pédrot
2015-10-27Indexing existentially quantified entries returned by interp_entry_name.Pierre-Marie Pédrot
2015-10-27Type-safe grammar extensions.Pierre-Marie Pédrot
2015-10-26Pcoq entries are given a proper module.Pierre-Marie Pédrot
2015-10-25Getting rid of the Atactic entry.Pierre-Marie Pédrot
2015-10-25Getting rid of the Agram entry.Pierre-Marie Pédrot
2015-10-21Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Pierre-Marie Pédrot
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-06-29Code documentation of the TACTIC/VERNAC EXTEND macros.Pierre-Marie Pédrot
2015-06-25Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-06-23Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-08A more user-friendly naming of variables of ltac names defined byHugo Herbelin
2015-02-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-19Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Pierre-Marie Pédrot
2015-02-19Record type for VERNAC EXTEND rules and a bit of documentation.Pierre-Marie Pédrot
2015-01-27Tentative fix for bug #3957.Pierre-Marie Pédrot
2015-01-23Splitting ML tactics in one function per grammar entry.Pierre-Marie Pédrot
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
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-16Fixing CAMLP4 compilation.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:35:57 +0000