aboutsummaryrefslogtreecommitdiff
path: root/library/declaremods.mli
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-16Specialize `ImportObject` to `Export`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-06-11Move type definition Nativecode.symbols to NativevaluesGaëtan Gilbert
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2018-10-26[libobject] Move object_name next to object definition.Emilio Jesus Gallego Arias
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-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-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-06-05LtacProf for Coq trunkJason Gross
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-07-10Native compiler: refactor code handling pre-computed values.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-10-13selective join/export of the safe_environmentEnrico Tassi
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-07-17Declaremods: major refactoring, stop duplicating libobjects in modulesletouzey
2013-07-17More dynamic argument scopesletouzey
2013-05-12Use the Hook module here and there.ppedrot
2013-04-15Minor simplifications in Declaremods and Safe_typingletouzey
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 5)letouzey
2013-02-19Dir_path --> DirPathletouzey
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-18Modulification of mod_bound_idppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-03-02Noise for nothingpboutill
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-02-11Annotations at functor applications:letouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 22:51:15 +0000