aboutsummaryrefslogtreecommitdiff
path: root/kernel/modops.ml
AgeCommit message (Expand)Author
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-01-20Update copyright headers.Maxime Dénès
2015-12-22Inclusion of functors with restricted signature is now forbidden (fix #3746)Pierre Letouzey
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-25Minor module cleanup : error HigherOrderInclude was never happeningPierre Letouzey
2015-10-02Univs: uncovered bug in strengthening of opaque polymorphic definitions.Matthieu Sozeau
2015-03-25Fix vm compiler to refuse to compile code making use of inductives withMatthieu Sozeau
2015-03-18More sharing in module substitution.Pierre-Marie Pédrot
2015-02-12Univs: fix bug #3978: carry around the universe context used toMatthieu Sozeau
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2014-11-21Fix bug #3804.Matthieu Sozeau
2014-11-12Cleaner interfaces for linking locations of native compiler.Maxime Dénès
2014-10-13selective join/export of the safe_environmentEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-02Implement module subtyping for polymorphic constants (errors onMatthieu Sozeau
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-14Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadPierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2013-12-28Removing native_name reference from constant_body.Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:43:19 +0000