aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.ml
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Returning instance instead of substitution in universe context abstraction.Gravatar Pierre-Marie Pédrot2017-12-30
* Using a dedicated type for Lib.abstr_info.Gravatar Pierre-Marie Pédrot2017-12-30
* [lib] [api] Introduce record for `object_prefix`Gravatar Emilio Jesus Gallego Arias2017-11-29
* [api] A few more minor deprecation notices.Gravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
* Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\
* | Print names of all open blocksGravatar Tej Chajed2017-08-06
| * [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
|/
* Getting rid of AUContext abstraction breakers in Discharge.Gravatar Pierre-Marie Pédrot2017-07-13
* Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* [lib] Remove obsolete state-management function add_frozen_stateGravatar Emilio Jesus Gallego Arias2017-06-12
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* [library] Refactor state handling.Gravatar Emilio Jesus Gallego Arias2017-03-14
* [library] Don't recompute path_prefix on unfreeze.Gravatar Emilio Jesus Gallego Arias2017-03-14
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\
| * Fix a bug of Mltop.declare_cache_object.Gravatar Pierre-Marie Pédrot2016-10-05
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\|
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
* | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
| * Remove dead code in library/lib.ml.Gravatar Maxime Dénès2016-09-20
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* | | Changing the definition of the "Lib.variable.info" type to enable us to do mo...Gravatar Matej Kosik2016-08-24
| |/ |/|
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Exporting section_segment_of_reference.Gravatar Hugo Herbelin2016-06-29
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\
| * Univs: fix for part #2 of bug #4816.Gravatar Matthieu Sozeau2016-06-13
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/
* Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* lib_stack: API to reorder the libstackGravatar Enrico Tassi2015-10-28
* Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesGravatar Matthieu Sozeau2015-10-27
* Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Update headers.Gravatar Maxime Dénès2015-01-12
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Fix Declaremods.end_library (Closes: #3536)Gravatar Enrico Tassi2014-09-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 07:32:41 +0000