aboutsummaryrefslogtreecommitdiff
path: root/library/declaremods.mli
AgeCommit message (Expand)Author
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
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-01-17Variant !F M for functor application that does not honor the Inline declarationsletouzey
2010-01-07Include can accept both Module and Module Typeletouzey
2009-12-07No more specific syntax "Include Self" for inclusion of partially-applied fun...letouzey
2009-11-18Module subtyping : allow many <: and module type declaration with <:letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:49:40 +0000