| Commit message (Expand) | Author | Age |
* | COMMENTS: added to the "Names" module. | Matej Kosik | 2015-12-18 |
* | Hashconsing modules. | Pierre-Marie Pédrot | 2015-11-15 |
* | Better debug printers for module paths. | Maxime Dénès | 2015-09-20 |
* | Display functions for primitive projections. | Maxime Dénès | 2015-07-02 |
* | Fixing bug #4190. | Pierre-Marie Pédrot | 2015-04-16 |
* | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau | 2015-01-15 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Fix (actually, properly implement :) hashconsing of projections, | Matthieu Sozeau | 2014-12-17 |
* | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Missing equalities in Names-like structures. | Pierre-Marie Pédrot | 2014-03-20 |
* | Using HMaps in global references. | Pierre-Marie Pédrot | 2014-03-08 |
* | Also use HMaps in KNmap. | Pierre-Marie Pédrot | 2014-03-08 |
* | Using Hashmaps by default in constant and inductive maps. This changes fold and | Pierre-Marie Pédrot | 2014-03-07 |
* | Inductive maps in Environ now use HMap. | Pierre-Marie Pédrot | 2014-03-06 |
* | Lazily computed hash in KerName.t. | Pierre-Marie Pédrot | 2014-03-05 |
* | Fixing generic hashes and replacing them with proper ones. | Pierre-Marie Pédrot | 2014-03-03 |
* | Allocation-friendly mapping functions in Nametab. | Pierre-Marie Pédrot | 2014-02-03 |
* | More monomorphic List.mem + List.assoc + ... | letouzey | 2013-10-24 |
* | Specializing hash functions for widely used types. | ppedrot | 2013-10-24 |
* | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey | 2013-10-23 |
* | Added a more efficient way to recover the domain of a map. | ppedrot | 2013-08-25 |
* | Declarations.mli: reorganization of modular structures | letouzey | 2013-08-20 |
* | Small fixes due to the arrival of OCaml 3.12. | ppedrot | 2013-08-03 |
* | Replacing Id.check with Id.is_valid, as its sole use was under | ppedrot | 2013-05-14 |
* | Removing Gmap from Extraction plugin | ppedrot | 2013-05-12 |
* | Minor cleanup concerning Mod_subst.MBImap | letouzey | 2013-04-02 |
* | Restrict (try...with...) to avoid catching critical exn (part 1) | letouzey | 2013-03-12 |
* | Names: shortcuts for building {kn, constant, mind} with empty sections | letouzey | 2013-02-26 |
* | Names: Modularize constant and mutual_inductive | letouzey | 2013-02-26 |
* | Dir_path --> DirPath | letouzey | 2013-02-19 |
* | module_path --> ModPath.t, kernel_name --> KerName.t | letouzey | 2013-02-19 |
* | Names: revised representation of constants and mutual_inductive | letouzey | 2013-02-19 |
* | Modulification of name | ppedrot | 2012-12-18 |
* | Modulification of mod_bound_id | ppedrot | 2012-12-18 |
* | Modulification of Label | ppedrot | 2012-12-18 |
* | Fixing ocalmdoc comment | ppedrot | 2012-12-14 |
* | Modulification of dir_path | ppedrot | 2012-12-14 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Moving hcons_string to String namespace. | ppedrot | 2012-12-14 |
* | Monomorphization (kernel) | ppedrot | 2012-11-22 |
* | More monomorphizations | ppedrot | 2012-11-13 |
* | Removed many calls to OCaml generic equality. This was done by | ppedrot | 2012-10-29 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Names : check of labels, cleanup, nicer debug display of kn and constant | letouzey | 2011-10-11 |
* | Hash-consing of constr could share more | letouzey | 2011-10-02 |
* | Hash-consing: attempt to stop hash-consing separately constr in declare.ml | letouzey | 2011-09-22 |
* | Names.make_mbid and co : convert from/to identifier (avoid some String.copy) | letouzey | 2011-09-15 |
* | More twicks on hash-consing | letouzey | 2011-09-08 |