coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-05-04	[ssr] get rid of (pf_)mkSsrConst	Enrico Tassi

2020-05-03	Further port of the SSR tactics.	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-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-04-23	[ssr] under: Fix the defective form ("=> [\|]" implied) and its doc	Erik Martin-Dorel
	* Add tests accordingly.
2019-04-23	[ssr] new syntax for the under tactic	Enrico Tassi

2019-04-23	[ssr] over: Expose the new type of tactic for Ssrfwd.overtac	Erik Martin-Dorel

2019-04-23	[ssr] over: Add Ssrfwd.overtac in the .mli	Erik Martin-Dorel

2019-04-23	[ssr] under: Add support for one-liners "under (…) by [tac1\|tac2]."	Erik Martin-Dorel
	Supported syntax: under i: eq_bigr by rewrite adnnC. (* ensure 1 Under subogal is created ) under i: eq_big by [rewrite adnnC \| rewrite addnC]. ( 2 Under subgoals *) Equivalent, expanded form: under i: eq_bigr; [rewrite adnnC; over \| idtac]. under i: eq_big; [rewrite adnnC; over \| rewrite adnnC; over \| idtac].
2019-04-02	[ssr] implement "under i: ext_lemma" by rewrite rule	Enrico Tassi
	Still to do: renaming the bound variables afterwards
2019-01-18	[ssr] clean up implementation of {}/v -> /v{v}	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
	Ssripats and Ssrview are now written in the Tactic Monad. Ssripats implements the => tactical. Ssrview implements the application of forward views. The code is, according to my tests, 100% backward compatible. The code is much more documented than before. Moreover the "ist" (ltac context) used to interpret views is the correct one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC EXTEND execution time). Some of the code not touched by this commit still uses the incorrect ist, so its visibility in TACTIC EXTEND can't be removed yet. The main changes in the code are: - intro patterns are implemented using a state machine (a goal comes with a state). Ssrcommon.MakeState provides an easy way for a tactic to enrich the goal with with data of interest, such as the set of hyps to be cleared. This cleans up the old implementation that, in order to thread the state, that to redefine a bunch of tclSTUFF - the interpretation of (multiple) forward views uses the state to accumulate intermediate results - the bottom of Sscommon collects a bunch of utilities written in the tactic monad. Most of them are the rewriting of already existing utilities. When possible the old version was removed.
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