coq - The formal proof system

Age	Commit message (Expand)	Author
2019-04-29	Merge PR #9651: [ssr] Add tactics under and over	Cyril Cohen
2019-04-23	[ssr] set under's tactic argument at LEVEL 3	Erik Martin-Dorel
2019-04-23	[ssr] under: Fix the defective form ("=> [\|]" implied) and its doc	Erik Martin-Dorel
2019-04-23	[ssr] new syntax for the under tactic	Enrico Tassi
2019-04-23	[ssr] under: Add support for one-liners "under (…) by [tac1\|tac2]."	Erik Martin-Dorel
2019-04-16	Clean the representation of recursive annotation in Constrexpr	Maxime Dénès
2019-04-02	[ssr] implement "under i: ext_lemma" by rewrite rule	Enrico Tassi
2019-04-02	Add parsing of decimal constants (e.g., 1.02e+01)	Pierre Roux
2019-04-02	Rename the INT token to NUMERAL	Pierre Roux
2019-04-01	Replace type sign = bool with SPlus \| SMinus	Pierre Roux
2019-03-20	Stop accessing proof env via Pfedit in printers	Maxime Dénès
2019-02-11	[ssr] keep user annotation on views (fix #9538)	Enrico Tassi
2019-01-21	[ssr] cleanup of some comments	Enrico Tassi
2019-01-18	[ssr] clean up implementation of {}/v -> /v{v}	Enrico Tassi
2018-12-18	[ssr] make > a stand alone intro pattern	Enrico Tassi
2018-12-18	[ssr] extended intro patterns: + > [^] /ltac:	Enrico Tassi
2018-11-28	Merge PR #9070: [ssreflect] Export more parsing witnesses.	Enrico Tassi
2018-11-27	Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...	Emilio Jesus Gallego Arias
2018-11-26	[ssreflect] Export more parsing witnesses.	Emilio Jesus Gallego Arias
2018-11-23	Remove the unsafe camlp5 API from the Coq codebase.	Pierre-Marie Pédrot
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert
2018-11-17	[ltac] Use CAst nodes in the tactic AST.	Emilio Jesus Gallego Arias
2018-10-31	[ssr] use tclDISPATCH for IPatDispatch (fix #8544)	Enrico Tassi
2018-10-15	Port remaining EXTEND ml4 files to coqpp.	Pierre-Marie Pédrot