coq - The formal proof system

Age	Commit message (Expand)	Author
2019-05-13	Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.	Hugo Herbelin
2019-05-13	Moving Evd.evars_of_term from constr to econstr + consequences.	Hugo Herbelin
2019-04-10	Remove one call to Global.env in Detyping	Maxime Dénès
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-01-18	[ssr] clean up implementation of {}/v -> /v{v}	Enrico Tassi
2018-12-18	[ssr] extended intro patterns: + > [^] /ltac:	Enrico Tassi
2018-12-12	Higher-level libobject API for objects with fixed scopes	Maxime Dénès
2018-06-22	[ssr] implement {}/v as a short hand for {v}/v when v is an id	Enrico Tassi
2018-06-12	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias
2018-05-16	[ssr] fix after to_constr ~abort_on_undefined_evars was added	Enrico Tassi
2018-04-13	Evar maps contain econstrs.	Gaëtan Gilbert
2018-03-31	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias
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-28	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias
2018-02-27	Update headers following #6543.	Théo Zimmermann
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-16	Removing Proof_type from the API.	Pierre-Marie Pédrot
2017-06-07	Put "ssreflect" behind "API".	Matej Košík
2017-06-06	Merge the ssr plugin.	Maxime Dénès