aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
AgeCommit message (Expand)Author
2014-12-17Ensuring the good invariants of hashcons table generation in the API.Pierre-Marie Pédrot
2014-12-17Fix (actually, properly implement :) hashconsing of projections,Matthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
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-05Canary testing absence of generic equality for KerNamesPierre-Marie Pédrot
2014-03-05Lazily computed hash in KerName.t.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-03Kernel names are implemented using records.Pierre-Marie Pédrot
2014-02-03Allocation-friendly mapping functions in Nametab.Pierre-Marie Pédrot
2013-10-31Fixing Kerpair.hash. Since the beginning, it dit not respect the typeppedrot
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-22More complete hashcons : lists (dirpath), arrays (constr)letouzey
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-05-14Replacing Id.check with Id.is_valid, as its sole use was underppedrot
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-21Names: con_modpath and con_label access back the user kn partletouzey
2013-02-19avoid (Int.equal (cmp ...) 0) when a boolean equality existsletouzey
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-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-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-11-08Removing another bunch of generic equalitiesppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-09-27Default hashconsing of identifiers.ppedrot
2012-09-26Cleaning, renaming obscure functions and documenting in Hashcons.ppedrot
2012-09-25Fixing ocamldoc errorsppedrot
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-08-08Updating headers.herbelin
2012-04-15Adding newline after warning and restoring distinction betweenherbelin
2012-04-05Shortcuts and optimizations of comparisonsxclerc