aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nametab.mli
Commit message (Expand)AuthorAge
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* Pour satisfaire ProofGeneralGravatar coq2003-01-31
* Export M + Module M <: SIGGravatar coq2003-01-09
* Affichage nom le plus court pour Syntactic DefinitionGravatar herbelin2002-11-26
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Un peu (plus) d'ordre dans Nametab...Gravatar coq2002-09-24
* Nametab data structure reorganisationGravatar coq2002-09-24
* Pretty-printing preliminaire des modules, commandesGravatar coq2002-08-19
* Petites corrections ici et laGravatar coq2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Re-installation de l'affichage des globaux par des noms courtsGravatar herbelin2001-11-19
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...Gravatar herbelin2001-10-12
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Nettoyage des commentairesGravatar herbelin2001-09-20
* Nettoyage des commentairesGravatar herbelin2001-09-20
* Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...Gravatar herbelin2001-09-19
* Suppression des library roots, on teste si un nom est absolu autrementGravatar herbelin2001-09-07
* ParsingGravatar herbelin2001-08-10
* Ajout error_global_not_foundGravatar herbelin2001-08-05
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Meilleur traitement des noms explicites dans la Nametab; Différentation du t...Gravatar herbelin2001-02-05
* Test pour empêcher 2 sections de même nomsGravatar herbelin2000-12-20
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de l...Gravatar herbelin2000-12-05
* Enregistrement des racines de la bibliothèqueGravatar herbelin2000-11-29
* NettoyageGravatar herbelin2000-11-26
* Prise en compte de noms absolus dans la nametabGravatar herbelin2000-11-26
* Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabGravatar filliatr2000-11-24
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* implicites manuelsGravatar filliatr2000-11-21
* Nouvelle structure arborescente à la Nametab pour prendre en compte les noms...Gravatar herbelin2000-11-20
* juste l'interface de DischargeGravatar filliatr1999-09-28
* - un effort sur la doc (ocamlweb)Gravatar filliatr1999-09-19