index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
declaremods.mli
Commit message (
Expand
)
Author
Age
*
Modules and ppvernac, sequel of Enrico's commit 16261
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 5)
letouzey
2013-03-13
*
Dir_path --> DirPath
letouzey
2013-02-19
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
remove many excessive open Util & Errors in mli's
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Print Module (Type) M now tries to print more details
letouzey
2011-05-11
*
Annotations at functor applications:
letouzey
2011-02-11
*
A fine-grain control of inlining at functor application via priority levels
letouzey
2011-01-31
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Variant !F M for functor application that does not honor the Inline declarations
letouzey
2010-01-17
*
Include can accept both Module and Module Type
letouzey
2010-01-07
*
No more specific syntax "Include Self" for inclusion of partially-applied fun...
letouzey
2009-12-07
*
Module subtyping : allow many <: and module type declaration with <:
letouzey
2009-11-18
*
New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))
letouzey
2009-11-16
*
Include Self (Type) Foo: applying a (Type) Functor to the current context
letouzey
2009-11-16
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
DISCLAIMER
puech
2009-01-17
*
Enhancements to coqdoc, better globalization of sections and modules.
msozeau
2008-06-06
*
Beaoucoup de changements dans la representation interne des modules.
soubiran
2008-02-01
*
Keep ClosedSection marker for reset
herbelin
2005-02-20
*
Code mort
herbelin
2005-02-18
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
- Module/Declare Module syntax made more uniform:
sacerdot
2005-01-06
*
Nouvelle en-tĂȘte
herbelin
2004-07-16
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Export process_module_bindings pour traducteur
herbelin
2003-09-02
*
Export M + Module M <: SIG
coq
2003-01-09
*
Petit netoyage dans lib
coq
2002-12-19
*
La notation with dependante + affichage dependante de moduels corrige
coq
2002-09-20
*
Modules dans COQ\!\!\!\!
coq
2002-08-02