aboutsummaryrefslogtreecommitdiff
path: root/vernac/lemmas.mli
AgeCommit message (Expand)Author
2018-02-01[vernac] Mutual theorems (VernacStartTheoremProof) always have namesVincent Laporte
2017-12-13[econstr] Small cleanup in `vernac/lemmas`Emilio Jesus Gallego Arias
2017-11-29[proof] [api] Rename proof types in preparation for functionalization.Emilio Jesus Gallego Arias
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-13[api] Insert miscellaneous API deprecation back to core.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Maxime Dénès
2017-04-09Fixing #5420 as well as many related bugs due to miscounting let-ins.Hugo Herbelin
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias