aboutsummaryrefslogtreecommitdiff
path: root/kernel/modops.ml
AgeCommit message (Expand)Author
2020-04-20Remove mod_constraints field of module bodyGaëtan Gilbert
2020-03-26Fix #11845: anomaly when including partially applied functorGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17Allow to delay polymorphic opaque constants.Pierre-Marie Pédrot
2019-05-23Fixing typos - Part 2JPR
2019-05-14Reduce the attack surface of Opaqueproof.Pierre-Marie Pédrot
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-16Print full binders in subtyping incompatible polymorphism error.Gaëtan Gilbert
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-07-03Modops.add_retroknowledge: remove unused argument.Gaëtan Gilbert
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
2018-06-07Fix #7615: Functor inlining drops universe substitution.Pierre-Marie Pédrot
2018-05-23Renaming miscellaneous internal smart functions.Hugo Herbelin
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-08-29Statically enforcing that module types have no retroknowledge.Pierre-Marie Pédrot
2017-08-29Separating the module_type and module_body types by using a type parameter.Pierre-Marie Pédrot
2017-07-11Properly handling polymorphic inductive subtyping in the kernel.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:09:01 +0000