aboutsummaryrefslogtreecommitdiff
path: root/library/declaremods.ml
AgeCommit message (Expand)Author
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
2014-12-25Forbid Require inside interactive modules and module types.Maxime Dénès
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-10-13selective join/export of the safe_environmentEnrico Tassi
2014-09-02Fix Declaremods.end_library (Closes: #3536)Enrico Tassi
2014-05-01Fixing ml-doc.Pierre-Marie Pédrot
2014-03-18STM: make -async-proofs on work from coqc tooEnrico Tassi
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2013-11-22Using hashes instead of strings in dynamic tags. In case of collision, anPierre-Marie Pédrot
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-20Safe_typing code refactoringletouzey
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 16:39:21 +0000