aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/indschemes.ml
Commit message (Expand)AuthorAge
* 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