aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/grammar.mllib
Commit message (Expand)AuthorAge
* Further reducing the dependencies of the EXTEND macros.Gravatar Pierre-Marie Pédrot2016-03-19
* Removing dead code in Pcoq.Gravatar Pierre-Marie Pédrot2016-03-18
* Making the EXTEND macros almost self-contained.Gravatar Pierre-Marie Pédrot2016-03-18
* Reducing the number of modules linked in grammar.cma.Gravatar Pierre-Marie Pédrot2016-03-17
* Expurging grammar.mllib from uselessly linked modules.Gravatar Pierre-Marie Pédrot2016-03-06
* Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.Gravatar Pierre-Marie Pédrot2016-03-06
* Removing the Q_coqast module.Gravatar Pierre-Marie Pédrot2016-02-24
* Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\
| * Fix order of files in mllib.Gravatar Maxime Dénès2016-01-05
* | Factorizing unsafe code by relying on the new Dyn module.Gravatar Pierre-Marie Pédrot2015-12-05
* | Pcoq entries are given a proper module.Gravatar Pierre-Marie Pédrot2015-10-26
| * Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
* | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-23
|/
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Adding a canary library. This canary is imperfect. It allows serializationGravatar Pierre-Marie Pédrot2014-03-05
* Added a new module HMap. It works (almost) like Map, except that it expectsGravatar Pierre-Marie Pédrot2014-03-05
* Adding a CSet module in Coq lib.Gravatar Pierre-Marie Pédrot2014-03-05
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Moving Searchstack to CStack, and normalizing names a bit.Gravatar ppedrot2013-09-06
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Proof-of-concept: moved four easy-to-handle generic arguments toGravatar ppedrot2013-06-18
* Added a generic notion of hook. Hooks are functions to be setGravatar ppedrot2013-05-12
* Updated Exninfo to the new Store type.Gravatar ppedrot2013-03-12
* Added exception enrichment. Now one can define additional arbitraryGravatar ppedrot2013-02-18
* Added backtrace primitives.Gravatar ppedrot2013-01-28
* Moving hcons_string to String namespace.Gravatar ppedrot2012-12-14
* Implemented a full-fledged equality on [constr_expr]. By the way,Gravatar ppedrot2012-12-14
* Added a CString module.Gravatar ppedrot2012-11-13
* Added an Int module with dummy utility functions.Gravatar ppedrot2012-11-08
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Reusing the Hashset data structure in Hashcons. Hopefully, this shouldGravatar ppedrot2012-09-26
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Extend become a mli-only file in intf/Gravatar letouzey2012-05-29
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 22:48:55 +0000