aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_typing.ml
Commit message (Expand)AuthorAge
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Mod_typing : code cleanupGravatar letouzey2013-08-20
* Safe_typing code refactoringGravatar letouzey2013-08-20
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Modops.destr_functor without useless envGravatar letouzey2013-07-17
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of LabelGravatar ppedrot2012-12-18
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* Noise for nothingGravatar pboutill2012-03-02
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
* Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneGravatar letouzey2011-04-12
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Moving printing of module typing errors upwards to himsg.ml so as toGravatar herbelin2011-03-05
* Mod_typing: some refactoring (common parts about MSEapply and co)Gravatar letouzey2011-02-11
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Mod_typing: fix the content of the typ_expr_alg fieldGravatar letouzey2010-07-07
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* cf. 12945Gravatar soubiran2010-04-16
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Module type expressions of the form (Fsig X) with Definition foo := bar are n...Gravatar soubiran2009-10-28
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* retour sur le commit 11579 qui faisait plante les contribs FSet et color.Gravatar soubiran2008-11-14
* Les signatures des applications de foncteur sont précalculées, cela alourdi...Gravatar soubiran2008-11-12
* Correction bug 1979.Gravatar soubiran2008-10-28
* Correction bug #1969.Gravatar soubiran2008-10-21
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* Les contraintes d'univers sont maintenant collectées dans le champs mod_cons...Gravatar soubiran2008-06-25
* meilleur gestion de la fonction de "cache" des alias (declaremods), et correc...Gravatar soubiran2008-06-18
* correction bug 1839Gravatar soubiran2008-04-25
* correction d'un bug sur la compostion des substitutions induites par les alia...Gravatar soubiran2008-04-23
* correction bug 1839Gravatar soubiran2008-04-22
* fixed universes bug related to module inclusionGravatar barras2008-04-22
* Patch sur le typage d'un foncteur applique a un alias.Gravatar soubiran2008-04-03
* Correction de bugs relatifs a la compostion des substitutionsGravatar soubiran2008-03-25
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11