aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
AgeCommit message (Expand)Author
2012-04-15Adding newline after warning and restoring distinction betweenherbelin
2012-04-05Shortcuts and optimizations of comparisonsxclerc
2012-03-02Noise for nothingpboutill
2011-10-11Names : check of labels, cleanup, nicer debug display of kn and constantletouzey
2011-10-10Avoid some re-allocation during hash-cons of dir_pathletouzey
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-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-10-03Fixing printing of module_path names (was using a debuggingherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-23Names: remove obsolete mod_self_idletouzey
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-04-29After the approval of Bruno, here the patch for the checker.soubiran
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-08Some dead code removal + cleanupsletouzey
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
2008-10-15Report des commits 11417 et 11437 de la v8.2soubiran
2008-07-15Autour du parsing:herbelin
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-21- Parameterize unification by two sets of transparent_state, one for openmsozeau
2008-04-14suite 10790 (identificateurs)herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2007-12-18Nettoyage de code en vue de la release. Plus de Warning: Unused aspiwack
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2007-02-21Fixed the pseudo-cicularity problem due to the with operator on Module Type.soubiran
2007-01-24modifications des messages d'erreurs renvoyés lors de la comparaison soubiran
2006-05-23Modification de add_glob (support des modules dans Coqdoc)notin
2006-01-11Suppression résidus code v7 et traducteurherbelin
2005-02-18Moved Indmap and ConstrMap from Libnames to Names for use in Cookingherbelin
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-07-16Nouvelle en-têteherbelin
2004-03-28Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans coqt...herbelin
2003-03-12*** empty log message ***barras
2003-01-31*** empty log message ***courant
2003-01-22id_of_msid en plusletouzey
2002-12-09Corrections de gestion des univers et modules + meilleure gestions des noms...coq
2002-12-05des Set et des Map en plusletouzey
2002-12-04Corrige un bug de composition de substitutionscoq
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-09-29Hash-consing pour kernel_nameherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:47:18 +0000