| Age | Commit message (Expand) | Author |
|---|
| 2016-12-02 | Fix #5242 - Dubious unsilenceable warning on invalid identifier | Maxime Dénès |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias |
| 2016-05-08 | Removing dead code and unused opens. | Pierre-Marie Pédrot |
| 2016-03-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-03-22 | A patch renaming equal into eq in the module dealing with | Hugo Herbelin |
| 2016-03-22 | Adding eq/compare/hash for syntactic view at | Hugo Herbelin |
| 2016-02-18 | ADD: Names.Name.is_{anonymous,name} | Matej Kosik |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-11 | COMMENTS: added to the "Names.inductive" and "Names.constructor" types. | Matej Kosik |
| 2015-12-18 | COMMENTS: added to the "Names" module. | Matej Kosik |
| 2015-09-20 | Better debug printers for module paths. | Maxime Dénès |
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | A patch renaming equal into eq in the module dealing with | Hugo Herbelin |
| 2015-08-02 | Adding eq/compare/hash for syntactic view at | Hugo Herbelin |
| 2015-07-30 | Followup of 9f81b58551. | Pierre-Marie Pédrot |
| 2015-07-30 | Fixing bug #4289 (hash-consing only user part of constant not | Hugo Herbelin |
| 2015-07-02 | Display functions for primitive projections. | Maxime Dénès |
| 2015-04-16 | Fixing bug #4190. | Pierre-Marie Pédrot |
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot |
| 2015-01-15 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-12-17 | Ensuring the good invariants of hashcons table generation in the API. | Pierre-Marie Pédrot |
| 2014-12-17 | Fix (actually, properly implement :) hashconsing of projections, | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-03-20 | Missing equalities in Names-like structures. | Pierre-Marie Pédrot |
| 2014-03-08 | Using HMaps in global references. | Pierre-Marie Pédrot |
| 2014-03-08 | Also use HMaps in KNmap. | Pierre-Marie Pédrot |
| 2014-03-07 | Using Hashmaps by default in constant and inductive maps. This changes fold and | Pierre-Marie Pédrot |
| 2014-03-05 | Canary testing absence of generic equality for KerNames | Pierre-Marie Pédrot |
| 2014-03-05 | Lazily computed hash in KerName.t. | Pierre-Marie Pédrot |
| 2014-03-05 | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2014-03-03 | Kernel names are implemented using records. | Pierre-Marie Pédrot |
| 2014-02-03 | Allocation-friendly mapping functions in Nametab. | Pierre-Marie Pédrot |
| 2013-10-31 | Fixing Kerpair.hash. Since the beginning, it dit not respect the type | ppedrot |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-24 | Specializing hash functions for widely used types. | ppedrot |
| 2013-10-23 | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey |
| 2013-08-25 | Added a more efficient way to recover the domain of a map. | ppedrot |
| 2013-08-22 | More complete hashcons : lists (dirpath), arrays (constr) | letouzey |
| 2013-08-20 | Declarations.mli: reorganization of modular structures | letouzey |
| 2013-05-14 | Replacing Id.check with Id.is_valid, as its sole use was under | ppedrot |
| 2013-04-02 | Minor cleanup concerning Mod_subst.MBImap | letouzey |
| 2013-03-12 | Restrict (try...with...) to avoid catching critical exn (part 1) | letouzey |
| 2013-02-26 | Names: shortcuts for building {kn, constant, mind} with empty sections | letouzey |
| 2013-02-26 | Names: Modularize constant and mutual_inductive | letouzey |
| 2013-02-21 | Names: con_modpath and con_label access back the user kn part | letouzey |
