aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.ml
Commit message (Expand)AuthorAge
* 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
* 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
* 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
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Removing another bunch of generic equalitiesGravatar ppedrot2012-11-08
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
* Default hashconsing of identifiers.Gravatar ppedrot2012-09-27
* Cleaning, renaming obscure functions and documenting in Hashcons.Gravatar ppedrot2012-09-26
* Fixing ocamldoc errorsGravatar ppedrot2012-09-25
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Adding newline after warning and restoring distinction betweenGravatar herbelin2012-04-15
* Shortcuts and optimizations of comparisonsGravatar xclerc2012-04-05
* Noise for nothingGravatar pboutill2012-03-02
* Names : check of labels, cleanup, nicer debug display of kn and constantGravatar letouzey2011-10-11
* Avoid some re-allocation during hash-cons of dir_pathGravatar letouzey2011-10-10
* 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
* 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
* Fixing printing of module_path names (was using a debuggingGravatar herbelin2010-10-03
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Names: remove obsolete mod_self_idGravatar letouzey2010-06-23
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* After the approval of Bruno, here the patch for the checker.Gravatar soubiran2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* Autour du parsing:Gravatar herbelin2008-07-15
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21