aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.mli
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
* [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
* [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
* 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
* 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
* | Changing the definition of the "Lib.variable.info" type to enable us to do mo...Gravatar Matej Kosik2016-08-24
|/
* Exporting section_segment_of_reference.Gravatar Hugo Herbelin2016-06-29
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * 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
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/
* 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
* 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
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Lib.contents () instead of Lib.contents_after NoneGravatar letouzey2013-07-17
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Fix issues with "Reset Initial" in scripts given to coqtop -lGravatar letouzey2013-04-23
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Assumption commands are now displayed as unsafe in Coqide.Gravatar aspiwack2012-08-24
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29