aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/indschemes.ml
Commit message (Expand)AuthorAge
* [vernac] Add option to force building really mutual induction schemesGravatar Matthieu Sozeau2018-06-13
* Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* Deprecate UState aliases in Evd.Gravatar Gaëtan Gilbert2018-03-06
* Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\
| * [compat] Remove NOOP and alias deprecated options.Gravatar Emilio Jesus Gallego Arias2018-03-04
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
* When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
* Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
* Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
* [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
* Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
* Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
* More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
* Safer API for Global.type_of_global_in_context.Gravatar Pierre-Marie Pédrot2017-07-13
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove options deprecated since 8.4.Gravatar Guillaume Melquiond2017-06-14
* Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Pretyping cleanup: remove constr_of_global callsGravatar Matthieu Sozeau2017-05-29
* Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\
| * [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
| * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 00:14:44 +0000