aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/lemmas.mli
Commit message (Expand)AuthorAge
* [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [vernac] Mutual theorems (VernacStartTheoremProof) always have namesGravatar Vincent Laporte2018-02-01
* [econstr] Small cleanup in `vernac/lemmas`Gravatar Emilio Jesus Gallego Arias2017-12-13
* [proof] [api] Rename proof types in preparation for functionalization.Gravatar Emilio Jesus Gallego Arias2017-11-29
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
* Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
|\
| * Fixing #5420 as well as many related bugs due to miscounting let-ins.Gravatar Hugo Herbelin2017-04-09
* | 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-24 06:44:55 +0000