coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-01-20	Remove double induction tactic	Jim Fehrle

2020-11-20	Use nat_or_var where negative values don't make sense	Jim Fehrle

2020-10-14	Deprecating wit_var to the benefit of its synonymous wit_hyp.	Hugo Herbelin
	Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
2020-09-17	Formally deprecate the double induction tactic.	Pierre-Marie Pédrot
	The doc states it is deprecated since 1386cd9 but this was ages before the deprecation mechanism existed.
2020-05-19	Delay evaluating arguments of the "exists" tactic	Attila Gáspár

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-19	Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations ↵	Théo Zimmermann
	in favor of "simple_intropattern" Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-06-16	Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern".	Hugo Herbelin
	This is to prevent confusion with the terminology used in the grammar of tactic in the reference manual: "intropattern" in Tactic Notation and TACTIC EXTEND is actually bound to simple_intropattern and not to what is called intropattern in the reference manual After some deprecation phase, "intropattern" could be added back to mean the "intropattern" of the reference manual. Note that "simple_intropattern" is actually already available in "Tactic Notation" with the correct meaning as an entry. Only "intropattern" is misguiding.
2018-11-17	[ltac] Use CAst nodes in the tactic AST.	Emilio Jesus Gallego Arias
	This provides several advantages to people serializing tactic scripts. Appearance of the involved constructors is common enough as to bother to submit this PR.
2018-07-02	Remove the hardcoded compatibility wit_hyp -> wit_var from the parser.	Pierre-Marie Pédrot

2018-07-02	Moving various ml4 files to mlg.	Pierre-Marie Pédrot