aboutsummaryrefslogtreecommitdiff
path: root/interp/modintern.ml
AgeCommit message (Expand)Author
2010-01-07Include can accept both Module and Module Typeletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin
2008-06-14Correction bug 1878 (utilisation de extend_evar déplacée là où uneherbelin
2008-06-06Enhancements to coqdoc, better globalization of sections and modules.msozeau
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2005-01-13Construct "T with (Definition|Module) id := c" generalized tosacerdot
2004-07-16Nouvelle en-têteherbelin
2004-01-02meilleure presentation des commentaires du traducteurbarras
2002-11-14Réforme de l'interprétation des termes :herbelin