index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
modops.mli
Commit message (
Expand
)
Author
Age
*
Minor module cleanup : error HigherOrderInclude was never happening
Pierre Letouzey
2015-10-25
*
Update headers.
Maxime Dénès
2015-01-12
*
Cleaner interfaces for linking locations of native compiler.
Maxime Dénès
2014-11-12
*
selective join/export of the safe_environment
Enrico Tassi
2014-10-13
*
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-10-13
*
Implement module subtyping for polymorphic constants (errors on
Matthieu Sozeau
2014-10-02
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Removing native_name reference from constant_body.
Maxime Dénès
2013-12-28
*
Future: ported to Ephemeron + exception enhancing
gareuselesinge
2013-10-18
*
Declarations.mli: reorganization of modular structures
letouzey
2013-08-20
*
Declareops + Modops : more clever substitutions
letouzey
2013-08-20
*
Safe_typing code refactoring
letouzey
2013-08-20
*
enhance marshallable option for freeze (minor TODO in safe_typing)
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Modops.destr_functor without useless env
letouzey
2013-07-17
*
Robust display of NotConvertibleTypeField errors (fix #3008, #2995)
letouzey
2013-03-21
*
Fixing bug #2466
ppedrot
2013-02-24
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of identifier
ppedrot
2012-12-14
*
Updating headers.
herbelin
2012-08-08
*
remove many excessive open Util & Errors in mli's
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Modops: the strengthening functions can work without any env argument
letouzey
2011-05-17
*
Moving printing of module typing errors upwards to himsg.ml so as to
herbelin
2011-03-05
*
Starting being more explicit on the reasons why module subtyping fails.
herbelin
2011-03-05
*
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
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
cf. 12945
soubiran
2010-04-16
*
Include can accept both Module and Module Type
letouzey
2010-01-07
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Ajout des alias de module dans le noyau.
soubiran
2008-03-14
*
Attempt of fix for extraction of modules types
letouzey
2008-03-05
*
Beaoucoup de changements dans la representation interne des modules.
soubiran
2008-02-01
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
Fixed the pseudo-cicularity problem due to the with operator on Module Type.
soubiran
2007-02-21
*
modifications des messages d'erreurs renvoyés lors de la comparaison
soubiran
2007-01-24
*
Inversion de l'ordre de chargement des objets logiques et non logiques
herbelin
2006-04-15
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Construct "T with (Definition|Module) id := c" generalized to
sacerdot
2005-01-13
*
HUGE COMMIT
sacerdot
2005-01-03
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
Bug 'with Module' corrige
coq
2003-01-22
*
Contexte locale non-vide interdit a la fin d'un module ou module type
coq
2002-12-18
[next]