coq - The formal proof system

Age	Commit message (Expand)	Author
2019-05-10	Make the check flag of conversion functions mandatory.	Pierre-Marie Pédrot
2019-04-23	[ssr] under: Add iff support in side-conditions	Erik Martin-Dorel
2019-04-02	[ssr] fix implementation of refine ~first_goes_last	Enrico Tassi
2019-04-02	[ssr] move is_ind/constructor_ref to ssrcommon	Enrico Tassi
2019-03-14	Fix various dummy Relevant in ssr	Gaëtan Gilbert
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-01-19	[ssr] compile "=> {x..} y" as "=> {x..y} y"	Enrico Tassi
2018-12-18	[ssr] extended intro patterns: + > [^] /ltac:	Enrico Tassi
2018-11-28	[ltac] Remove aliases already present in the lower layers.	Emilio Jesus Gallego Arias
2018-11-21	[legacy proof engine] Remove some cruft.	Emilio Jesus Gallego Arias
2018-11-16	Remove SSR profiling	Jim Fehrle
2018-11-14	ssrcommon: API to call resolve_tyclasses on a term	Enrico Tassi
2018-10-24	[ssreflect] Better use of Coqlib	Vincent Laporte
2018-05-04	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias
2018-03-06	ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Enrico Tassi
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-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias
2017-06-16	Removing Proof_type from the API.	Pierre-Marie Pédrot
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