aboutsummaryrefslogtreecommitdiff
path: root/grammar
AgeCommit message (Expand)Author
2016-03-18ARGUMENT EXTEND made of only one entry share the same grammar.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic arguments defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Adding a universe argument to Pcoq.create_generic_entry.Pierre-Marie Pédrot
2016-03-17Removing the registering of default values for generic arguments.Pierre-Marie Pédrot
2016-03-17Removing dead code in Q_util.Pierre-Marie Pédrot
2016-03-17Reducing the number of modules linked in grammar.cma.Pierre-Marie Pédrot
2016-03-06Expurging grammar.mllib from uselessly linked modules.Pierre-Marie Pédrot
2016-03-06Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.Pierre-Marie Pédrot
2016-03-05Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".Pierre-Marie Pédrot
2016-03-04All arguments defined through ARGUMENT EXTEND declare a tactic scope.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:14:16 +0000