aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.mli
Commit message (Expand)AuthorAge
* 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
* Names: remove obsolete mod_self_idGravatar letouzey2010-06-23
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* After the approval of Bruno, here the patch for the checker.Gravatar soubiran2010-04-29
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Names.mli: double declaration of mind_modpathGravatar letouzey2010-04-16
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-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
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Fixed the pseudo-cicularity problem due to the with operator on Module Type.Gravatar soubiran2007-02-21
* modifications des messages d'erreurs renvoyés lors de la comparaison Gravatar soubiran2007-01-24
* Modification de add_glob (support des modules dans Coqdoc)Gravatar notin2006-05-23
* Moved Indmap and ConstrMap from Libnames to Names for use in CookingGravatar herbelin2005-02-18
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20