aboutsummaryrefslogtreecommitdiff
path: root/library/declaremods.ml
AgeCommit message (Expand)Author
2019-09-18[library] Move `Declaremods` to `vernac/`Emilio Jesus Gallego Arias
2019-09-16Optimize multiple importsMaxime Dénès
2019-09-16Optimize `Include`d `Export`sMaxime Dénès
2019-09-16Turn `module_objects` into a recordMaxime Dénès
2019-09-16Optimize module ExportsMaxime Dénès
2019-09-16Do not cache objects when importing modulesMaxime Dénès
2019-09-16Specialize `ImportObject` to `Export`Maxime Dénès
2019-09-16`do_modtype` -> `load_modtype`Maxime Dénès
2019-07-04Merge PR #10359: Remove dependency of native_compile on global env for symbolsMaxime Dénès
2019-06-28Reify libobject containersMaxime Dénès
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-12Remove dependency of native_compile on global env for symbolsGaëtan Gilbert
2019-05-23Fixing typos - Part 2JPR
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2018-12-13Move shallow state logic to the function preparing state for workersMaxime Dénès
2018-10-31[nametab] Move `object_prefix` to `Nametab`.Emilio Jesus Gallego Arias
2018-10-31[nametab] Move global_dir_reference to NametabEmilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: module_kind to DeclaremodsEmilio Jesus Gallego Arias
2018-04-06[api] Remove dependency of library on Vernacexpr.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-16Extrude monomorphic universe contexts from with Definition constraints.Pierre-Marie Pédrot
2017-11-29[lib] [api] Introduce record for `object_prefix`Emilio Jesus Gallego Arias
2017-11-21[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-12[lib] Remove obsolete state-management function add_frozen_stateEmilio Jesus Gallego Arias
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-05LtacProf for Coq trunkJason Gross
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-08Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03Fix bug #4292: Unexpected functor objects.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2015-12-05Leveraging GADTs to provide a better Dyn API.Pierre-Marie Pédrot
2015-10-25Declaremods: replace two anomalies by user errors (fix #3974 and #3975)Pierre Letouzey
2015-07-10Native compiler: refactor code handling pre-computed values.Maxime Dénès
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-01-17Partially revert "Forbid Require inside interactive modules and module types."Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:25:11 +0000