aboutsummaryrefslogtreecommitdiff
path: root/library/declaremods.mli
AgeCommit message (Expand)Author
2010-01-17Variant !F M for functor application that does not honor the Inline declarationsletouzey
2010-01-07Include can accept both Module and Module Typeletouzey
2009-12-07No more specific syntax "Include Self" for inclusion of partially-applied fun...letouzey
2009-11-18Module subtyping : allow many <: and module type declaration with <:letouzey
2009-11-16New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))letouzey
2009-11-16Include Self (Type) Foo: applying a (Type) Functor to the current contextletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-01-17DISCLAIMERpuech
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-02-20Keep ClosedSection marker for resetherbelin
2005-02-18Code mortherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-06- Module/Declare Module syntax made more uniform:sacerdot
2004-07-16Nouvelle en-têteherbelin
2004-01-02meilleure presentation des commentaires du traducteurbarras
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-09-02Export process_module_bindings pour traducteurherbelin
2003-01-09Export M + Module M <: SIGcoq
2002-12-19Petit netoyage dans libcoq
2002-09-20La notation with dependante + affichage dependante de moduels corrigecoq
2002-08-02Modules dans COQ\!\!\!\!coq
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:44:41 +0000