aboutsummaryrefslogtreecommitdiff
path: root/kernel/modops.ml
AgeCommit message (Expand)Author
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-20Declareops + Modops : more clever substitutionsletouzey
2013-08-20Safe_typing code refactoringletouzey
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-07-17Modops.destr_functor without useless envletouzey
2013-03-21Robust display of NotConvertibleTypeField errors (fix #3008, #2995)letouzey
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-24Fixing bug #2466ppedrot
2013-02-19Dir_path --> DirPathletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-11-13More monomorphizationsppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2011-10-26Mod_subst: some simplifications, some more significant names to functions, etcletouzey
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
2011-05-17Modops: the strengthening functions can work without any env argumentletouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-03-05Moving printing of module typing errors upwards to himsg.ml so as toherbelin
2011-03-05Starting being more explicit on the reasons why module subtyping fails.herbelin
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-11-15Minor fixes from Gregory Malecha. A typo fixed and a better (located) msozeau
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-16cf. 12945soubiran
2010-02-03fix commit 12706 + comments.soubiran
2010-02-02Small fix on module inclusion.soubiran
2010-01-07Include can accept both Module and Module Typeletouzey
2010-01-04The following script was rasing an errorsoubiran
2009-11-13the inlining computation at functor application was raising not_found when th...soubiran
2009-10-23First debug... the renaming of librairies was not working and auto/dn were no...soubiran
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-07-09Correction bug 2134.soubiran
2009-02-13Bug 2050, commit v8.2 11923-11924 ---> trunksoubiran
2008-10-28petite modif du commit 11513.soubiran
2008-10-28Correction bug 1979.soubiran
2008-10-21Correction bug #1969.soubiran
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:36:13 +0000