aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.ml
Commit message (Expand)AuthorAge
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\
| * A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2016-03-22
| * Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2016-03-22
* | ADD: Names.Name.is_{anonymous,name}Gravatar Matej Kosik2016-02-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Gravatar Matej Kosik2016-01-11
* | COMMENTS: added to the "Names" module.Gravatar Matej Kosik2015-12-18
* | Better debug printers for module paths.Gravatar Maxime Dénès2015-09-20
|/
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
* Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2015-08-02
* Followup of 9f81b58551.Gravatar Pierre-Marie Pédrot2015-07-30
* Fixing bug #4289 (hash-consing only user part of constant notGravatar Hugo Herbelin2015-07-30
* Display functions for primitive projections.Gravatar Maxime Dénès2015-07-02
* Fixing bug #4190.Gravatar Pierre-Marie Pédrot2015-04-16
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
* Fix (actually, properly implement :) hashconsing of projections,Gravatar Matthieu Sozeau2014-12-17
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Missing equalities in Names-like structures.Gravatar Pierre-Marie Pédrot2014-03-20
* Using HMaps in global references.Gravatar Pierre-Marie Pédrot2014-03-08
* Also use HMaps in KNmap.Gravatar Pierre-Marie Pédrot2014-03-08
* Using Hashmaps by default in constant and inductive maps. This changes fold andGravatar Pierre-Marie Pédrot2014-03-07
* Canary testing absence of generic equality for KerNamesGravatar Pierre-Marie Pédrot2014-03-05
* Lazily computed hash in KerName.t.Gravatar Pierre-Marie Pédrot2014-03-05
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Kernel names are implemented using records.Gravatar Pierre-Marie Pédrot2014-03-03
* Allocation-friendly mapping functions in Nametab.Gravatar Pierre-Marie Pédrot2014-02-03
* Fixing Kerpair.hash. Since the beginning, it dit not respect the typeGravatar ppedrot2013-10-31
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Specializing hash functions for widely used types.Gravatar ppedrot2013-10-24
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* More complete hashcons : lists (dirpath), arrays (constr)Gravatar letouzey2013-08-22
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Replacing Id.check with Id.is_valid, as its sole use was underGravatar ppedrot2013-05-14
* Minor cleanup concerning Mod_subst.MBImapGravatar letouzey2013-04-02
* Restrict (try...with...) to avoid catching critical exn (part 1)Gravatar letouzey2013-03-12
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Names: Modularize constant and mutual_inductiveGravatar letouzey2013-02-26
* Names: con_modpath and con_label access back the user kn partGravatar letouzey2013-02-21
* avoid (Int.equal (cmp ...) 0) when a boolean equality existsGravatar letouzey2013-02-19
* Dir_path --> DirPathGravatar letouzey2013-02-19