aboutsummaryrefslogtreecommitdiff
path: root/interp/modintern.mli
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-06Enhancements to coqdoc, better globalization of sections and modules.msozeau
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2004-07-16Nouvelle en-têteherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin