index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
mod_typing.mli
Age
Commit message (
Expand
)
Author
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-12-22
Inclusion of functors with restricted signature is now forbidden (fix #3746)
Pierre Letouzey
2015-10-25
Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)
Pierre Letouzey
2015-10-25
Minor module cleanup : error HigherOrderInclude was never happening
Pierre Letouzey
2015-10-02
Univs: module constraints move to universe contexts as they might
Matthieu Sozeau
2015-01-12
Update headers.
Maxime Dénès
2015-01-11
Declarations.mli refactoring: module_type_body = module_body
Pierre Letouzey
2013-08-20
Declarations.mli: reorganization of modular structures
letouzey
2012-08-08
Updating headers.
herbelin
2011-02-11
Mod_typing: some refactoring (common parts about MSEapply and co)
letouzey
2011-01-31
A fine-grain control of inlining at functor application via priority levels
letouzey
2010-07-24
Updated all headers for 8.3 and trunk
herbelin
2010-06-22
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-04-29
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-01-17
Variant !F M for functor application that does not honor the Inline declarations
letouzey
2009-10-21
This big commit addresses two problems:
soubiran
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2008-06-25
Les contraintes d'univers sont maintenant collectées dans le champs mod_cons...
soubiran
2008-04-22
fixed universes bug related to module inclusion
barras
2008-03-14
Ajout des alias de module dans le noyau.
soubiran
2008-02-01
Beaoucoup de changements dans la representation interne des modules.
soubiran
2005-01-21
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-03
HUGE COMMIT
sacerdot
2004-07-16
Nouvelle en-tête
herbelin
2002-08-02
Modules dans COQ\!\!\!\!
coq