aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/global.mli
Commit message (Expand)AuthorAge
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* 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
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Include Self (Type) Foo: applying a (Type) Functor to the current contextGravatar letouzey2009-11-16
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Nouveau mécanisme pour les modules interactifs : les arguments deGravatar herbelin2006-04-16
* Inversion de l'ordre de chargement des objets logiques et non logiquesGravatar herbelin2006-04-15
* *** empty log message ***Gravatar barras2006-01-20
* Changement des named_contextGravatar gregoire2005-12-02
* bug #909: Top n'est cree que si le contexte est videGravatar barras2005-11-23
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* Options -strongly-constructive et -strongly-classicalGravatar herbelin2003-10-28
* Corrections de gestion des univers et modules + meilleure gestions des noms...Gravatar coq2002-12-09
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* suppression de pop_namedGravatar barras2002-02-22
* Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantGravatar herbelin2001-11-20
* Mise en place d'une méthode directe pour indiquer le type des déclarations ...Gravatar herbelin2001-11-19
* Déplacement et export de type_of_global dans GlobalGravatar herbelin2001-11-09
* GROS COMMIT:Gravatar barras2001-11-05
* TransparentGravatar barras2001-09-20
* Mécanisme pour faire remonter les contraintes de typage sur les variables de...Gravatar herbelin2001-09-09
* ParsingGravatar herbelin2001-08-10
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Fonction qualid_of_global pour affichage des paths avec des '.'Gravatar herbelin2000-11-23
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* - environment -> safe_environmentGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01