aboutsummaryrefslogtreecommitdiff
path: root/grammar/grammar.mllib
AgeCommit message (Expand)Author
2016-06-08remove grammar/grammar.mllibPierre Letouzey
2016-05-31Making the grammar/ folder independent from the other ones.Pierre-Marie Pédrot
2016-03-19Further reducing the dependencies of the EXTEND macros.Pierre-Marie Pédrot
2016-03-18Removing dead code in Pcoq.Pierre-Marie Pédrot
2016-03-18Making the EXTEND macros almost self-contained.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-02-24Removing the Q_coqast module.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
2015-12-05Factorizing unsafe code by relying on the new Dyn module.Pierre-Marie Pédrot
2015-10-26Pcoq entries are given a proper module.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
2014-08-04STM: encapsulate Pp.message in Feedback.feedbackCarst Tankink
2014-06-25all coqide specific files moved into ide/Enrico Tassi
2014-03-05Adding a canary library. This canary is imperfect. It allows serializationPierre-Marie Pédrot
2014-03-05Added a new module HMap. It works (almost) like Map, except that it expectsPierre-Marie Pédrot
2014-03-05Adding a CSet module in Coq lib.Pierre-Marie Pédrot
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-07-02Removing the use of leveled tactics wit_tacticn. It is now handledppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-18Proof-of-concept: moved four easy-to-handle generic arguments toppedrot
2013-05-12Added a generic notion of hook. Hooks are functions to be setppedrot
2013-03-12Updated Exninfo to the new Store type.ppedrot
2013-02-18Added exception enrichment. Now one can define additional arbitraryppedrot
2013-01-28Added backtrace primitives.ppedrot
2012-12-14Moving hcons_string to String namespace.ppedrot
2012-12-14Implemented a full-fledged equality on [constr_expr]. By the way,ppedrot
2012-11-13Added a CString module.ppedrot
2012-11-08Added an Int module with dummy utility functions.ppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-09-26Reusing the Hashset data structure in Hashcons. Hopefully, this shouldppedrot
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29Extend become a mli-only file in intf/letouzey
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:46:43 +0000