coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| *	Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080	Jason Gross	2015-08-14
\|/
*	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
*	Add a [Redirect] vernacular command	Clément Pit--Claudel	2015-05-04
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Putting the From parameter of the Require command into the AST.	Pierre-Marie Pédrot	2015-03-27
*	Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior	Enrico Tassi	2015-02-14
*	Update headers.	Maxime Dénès	2015-01-12
*	Proof using: New vernacular to name sets of section variables	Enrico Tassi	2014-12-18
*	About now accepts hypothesis names and goal selector.	Pierre Courtieu	2014-12-15
*	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu	2014-12-12
*	Plug the dynamic tags in the Richpp mechanism.	Pierre-Marie Pédrot	2014-11-10
*	lib/RichPp: Rename into Richpp.	Yann Régis-Gianas	2014-11-05
*	printing/Ppvernac: Fix missing keyword tagging on theorem introducers.	Yann Régis-Gianas	2014-11-05
*	printing/Ppvernac: Fix missing keyword tagging on definition introducers.	Yann Régis-Gianas	2014-11-05
*	printing/Ppvernac: Cosmetics.	Yann Régis-Gianas	2014-11-05
*	printing/Ppannotation: New annotation for tactic syntactic objects.	Regis-Gianas	2014-11-04
*	Rebase artefact.	Regis-Gianas	2014-11-04
*	lib/Pp.tag: New.	Regis-Gianas	2014-11-04
*	printing/Ppannotation: Introduce a new annotation for keywords.	Regis-Gianas	2014-11-04
*	Ppannotation.t: New constructor AVernac.	Regis-Gianas	2014-11-04
*	Ppvernac.Make: New	Regis-Gianas	2014-11-04
*	Ppvernac: Cosmetics.	Regis-Gianas	2014-11-04
*	Add [Info] command.	Arnaud Spiwack	2014-11-01
*	Emit a warning for void Arguments statement (Close 3713)	Enrico Tassi	2014-10-13
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Notation: option to attach extra pretty printing rules to notations	Enrico Tassi	2014-09-29
*	Improve consistency of whitespace (beautifier).	Xavier Clerc	2014-09-25
*	Add a "Hint Mode ref (+ \| -)*" hint for setting a global mode	Matthieu Sozeau	2014-09-15
*	Add syntax [id]: to apply tactic to goal named id.	Hugo Herbelin	2014-09-12
*	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot	2014-09-10
*	Remove [Infer] option of records.	Arnaud Spiwack	2014-09-04
*	Add a [Variant] declaration which allows to write non-recursive variant types.	Arnaud Spiwack	2014-09-04
*	Improve consistency of whitespace (beautifier).	Xavier Clerc	2014-08-21
*	Improve consistency of whitespace (beautifier).	Xavier Clerc	2014-08-21
*	Space after [identity] coercion keywords (beautifier).	Xavier Clerc	2014-08-21
*	Avoid redundant spaces (beautifier).	Xavier Clerc	2014-08-21
*	Do not drop the locality qualifier (beautifier).	Xavier Clerc	2014-08-21
*	A couple of fixes/improvements in -beautify, but backtracking on	Hugo Herbelin	2014-08-12
*	Uncountably many bullets (+,-,,++,--,*,+++,...).	Hugo Herbelin	2014-08-05
*	Fixing a few beautifying bugs.	Hugo Herbelin	2014-08-05
*	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi	2014-08-05
*	Adding a new "Locate Term" command, distinct from the raw "Locate" command.	Pierre-Marie Pédrot	2014-07-21
*	Add toplevel commands to declare global universes and constraints.	Matthieu Sozeau	2014-07-01
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	- Add "Show Universes" to print information about universes during a proof.	Matthieu Sozeau	2014-06-16
*	Fix bug #3289	Matthieu Sozeau	2014-06-11
*	Remove the syntax [Vernac1. Vernac2. … Vernacn. ].	Arnaud Spiwack	2014-06-06
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Adding a Print Strategy vernacular command. It allows to check the	Pierre-Marie Pédrot	2014-03-19