coq - The formal proof system

Age	Commit message (Expand)	Author
2019-01-18	[ssr] clean up implementation of {}/v -> /v{v}	Enrico Tassi
2018-12-18	[ssr] make > a stand alone intro pattern	Enrico Tassi
2018-12-18	[ssr] extended intro patterns: + > [^] /ltac:	Enrico Tassi
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert
2018-08-13	Less crazy implementation of the "pose" family of tactics.	Pierre-Marie Pédrot
2018-07-19	Remove declare_object for SsrHave NoTCResolution.	Maxime Dénès
2018-06-22	[ssr] set: merge universe constraints before type checking the term	Enrico Tassi
2018-06-12	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias
2018-05-14	Deprecate Refiner [evar_map ref] exported functions.	Gaëtan Gilbert
2018-03-05	Merge PR #6855: Update headers following #6543.	Maxime Dénès
2018-03-04	ssr: rewrite Ssripats and Ssrview in the tactic monad	Enrico Tassi
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-11-22	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias
2017-11-21	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias
2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
2017-09-04	Making detyping potentially lazy.	Pierre-Marie Pédrot
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias
2017-06-10	Remove (useless) aliases from the API.	Matej Košík
2017-06-07	Put "ssreflect" behind "API".	Matej Košík
2017-06-06	Merge the ssr plugin.	Maxime Dénès