coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-05-03	Further port SSReflect tactics to the new engine.	Pierre-Marie Pédrot

2020-05-03	Wrap ssr tactics into V82.tactic.	Pierre-Marie Pédrot
	Porting them is still to be done, but at least we don't rely on the wrapper everywhere.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-08-06	[ssr] export Ssrequality.ssr_is_setoid	Erik Martin-Dorel

2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-04-02	[ssr] rewrite takes optional function to make the new valued of the redex	Enrico Tassi

2019-04-02	[ssr] clean up type declaration of ssrrewritetac	Enrico Tassi

2019-04-02	[ssr] under: rewrite takes an optional bool arg	Erik Martin-Dorel
	* If this flag under=true: enable flag with_evars of refine_with to create evar(s) if the "under lemma" has non-inferable args. * Backward compatibility of ssr rewrite is kept. * Fix test-suite/ssr/dependent_type_err.v
2018-02-27	Update headers following #6543.	Théo Zimmermann

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
	Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead.
2017-06-07	Put "ssreflect" behind "API".	Matej Košík

2017-06-06	Merge the ssr plugin.	Maxime Dénès