aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.mli
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-20Missing equalities in Names-like structures.Pierre-Marie Pédrot
2014-03-08Using HMaps in global references.Pierre-Marie Pédrot
2014-03-08Also use HMaps in KNmap.Pierre-Marie Pédrot
2014-03-07Using Hashmaps by default in constant and inductive maps. This changes fold andPierre-Marie Pédrot
2014-03-06Inductive maps in Environ now use HMap.Pierre-Marie Pédrot
2014-03-05Lazily computed hash in KerName.t.Pierre-Marie Pédrot
2014-03-03Fixing generic hashes and replacing them with proper ones.Pierre-Marie Pédrot
2014-02-03Allocation-friendly mapping functions in Nametab.Pierre-Marie Pédrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Specializing hash functions for widely used types.ppedrot
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-03Small fixes due to the arrival of OCaml 3.12.ppedrot
2013-05-14Replacing Id.check with Id.is_valid, as its sole use was underppedrot
2013-05-12Removing Gmap from Extraction pluginppedrot
2013-04-02Minor cleanup concerning Mod_subst.MBImapletouzey
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 1)letouzey
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-26Names: Modularize constant and mutual_inductiveletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-19module_path --> ModPath.t, kernel_name --> KerName.tletouzey
2013-02-19Names: revised representation of constants and mutual_inductiveletouzey
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Fixing ocalmdoc commentppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moving hcons_string to String namespace.ppedrot
2012-11-22Monomorphization (kernel)ppedrot
2012-11-13More monomorphizationsppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2011-10-11Names : check of labels, cleanup, nicer debug display of kn and constantletouzey
2011-10-02Hash-consing of constr could share moreletouzey
2011-09-22Hash-consing: attempt to stop hash-consing separately constr in declare.mlletouzey
2011-09-15Names.make_mbid and co : convert from/to identifier (avoid some String.copy)letouzey
2011-09-08More twicks on hash-consingletouzey
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-03-05Moving printing of module typing errors upwards to himsg.ml so as toherbelin
2011-02-11compatibility <3.12 (Map.exists Map.singleton)pboutill
2011-01-27Make simpl use the proper constant when folding (mutual) fixpointsletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-23Names: remove obsolete mod_self_idletouzey
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29After the approval of Bruno, here the patch for the checker.soubiran
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:05:23 +0000