aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/libnames.ml
Commit message (Expand)AuthorAge
* Rely on kernel to know if a name is already used so as to be consistent with it.Gravatar herbelin2011-10-08
* Print Module (Type) M now tries to print more detailsGravatar letouzey2011-05-11
* Added a table for using reserved names for binding names to typesGravatar herbelin2011-03-05
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* First debug... the renaming of librairies was not working and auto/dn were no...Gravatar soubiran2009-10-23
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
* Cleaning of Nametab continued + fixed a compilation bug in previous commit.Gravatar herbelin2009-08-06
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Correction bug 2037.Gravatar soubiran2009-01-30
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Lissage de la gestion des chemins de chargement de fichiers :Gravatar herbelin2008-06-29
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Rétablissement compatibilité constr_of_referenceGravatar herbelin2007-11-09
* Prise en compte des notations "alias" dans la globalisation des coercions.Gravatar herbelin2007-11-08
* Suite commit restructuration discharge (application du type deGravatar herbelin2007-01-10
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
* r8931@thot: notin | 2006-04-28 16:19:38 +0200Gravatar notin2006-04-28
* Ajout chop_dirpathGravatar herbelin2006-04-27
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* Standardisation of constr_of_reference into constr_of_global + Moved Indmap a...Gravatar herbelin2005-02-18
* HUGE COMMITGravatar sacerdot2005-01-03
* 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
* code mortGravatar herbelin2004-11-09
* Nouvelle en-têteGravatar herbelin2004-07-16
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...Gravatar herbelin2003-09-12
* Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...Gravatar herbelin2003-06-10
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* Mise en place d'un traducteur de noms v7->v8Gravatar herbelin2003-03-31
* des Set et des Map en plusGravatar letouzey2002-12-05
* Quelques Set et Map spécialisésGravatar letouzey2002-11-28
* Ajout RefmapGravatar herbelin2002-11-24
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 06:21:54 +0000