aboutsummaryrefslogtreecommitdiff
path: root/library/libnames.ml
AgeCommit message (Expand)Author
2011-03-05Added a table for using reserved names for binding names to typesherbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-23First debug... the renaming of librairies was not working and auto/dn were no...soubiran
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-08-07Fixed incorrect optimization in Prettyp.pr_located_qualid introducedherbelin
2009-08-06Cleaning of Nametab continued + fixed a compilation bug in previous commit.herbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-04-08Some dead code removal + cleanupsletouzey
2009-01-30Correction bug 2037.soubiran
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-06-29Lissage de la gestion des chemins de chargement de fichiers :herbelin
2008-02-22Merge with lmamane's private branch:lmamane
2007-11-09Rétablissement compatibilité constr_of_referenceherbelin
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2007-01-10Suite commit restructuration discharge (application du type deherbelin
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
2006-04-28 r8931@thot: notin | 2006-04-28 16:19:38 +0200notin
2006-04-27Ajout chop_dirpathherbelin
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type r...herbelin
2005-02-18Standardisation of constr_of_reference into constr_of_global + Moved Indmap a...herbelin
2005-01-03HUGE COMMITsacerdot
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-11-09code mortherbelin
2004-07-16Nouvelle en-têteherbelin
2003-09-12Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...herbelin
2003-06-10Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...herbelin
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...letouzey
2003-03-31Mise en place d'un traducteur de noms v7->v8herbelin
2002-12-05des Set et des Map en plusletouzey
2002-11-28Quelques Set et Map spécialisésletouzey
2002-11-24Ajout Refmapherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:22:13 +0000