aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.mli
Commit message (Expand)AuthorAge
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* 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
* Inductive maps in Environ now use HMap.Gravatar Pierre-Marie Pédrot2014-03-06
* Lazily computed hash in KerName.t.Gravatar Pierre-Marie Pédrot2014-03-05
* Fixing generic hashes and replacing them with proper ones.Gravatar Pierre-Marie Pédrot2014-03-03
* Allocation-friendly mapping functions in Nametab.Gravatar Pierre-Marie Pédrot2014-02-03
* 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
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Small fixes due to the arrival of OCaml 3.12.Gravatar ppedrot2013-08-03
* Replacing Id.check with Id.is_valid, as its sole use was underGravatar ppedrot2013-05-14
* Removing Gmap from Extraction pluginGravatar ppedrot2013-05-12
* 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
* Dir_path --> DirPathGravatar letouzey2013-02-19
* module_path --> ModPath.t, kernel_name --> KerName.tGravatar letouzey2013-02-19
* Names: revised representation of constants and mutual_inductiveGravatar letouzey2013-02-19
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Fixing ocalmdoc commentGravatar ppedrot2012-12-14
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Moving hcons_string to String namespace.Gravatar ppedrot2012-12-14
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* More monomorphizationsGravatar ppedrot2012-11-13
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
* Updating headers.Gravatar herbelin2012-08-08
* Noise for nothingGravatar pboutill2012-03-02
* Names : check of labels, cleanup, nicer debug display of kn and constantGravatar letouzey2011-10-11
* Hash-consing of constr could share moreGravatar letouzey2011-10-02
* Hash-consing: attempt to stop hash-consing separately constr in declare.mlGravatar letouzey2011-09-22
* Names.make_mbid and co : convert from/to identifier (avoid some String.copy)Gravatar letouzey2011-09-15
* More twicks on hash-consingGravatar letouzey2011-09-08
* Print Module (Type) M now tries to print more detailsGravatar letouzey2011-05-11
* Moving printing of module typing errors upwards to himsg.ml so as toGravatar herbelin2011-03-05
* compatibility <3.12 (Map.exists Map.singleton)Gravatar pboutill2011-02-11
* Make simpl use the proper constant when folding (mutual) fixpointsGravatar letouzey2011-01-27
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24