coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...	Matej Kosik	2015-12-18
* \|	CLEANUP: Vernacexpr.vernac_expr	Matej Kosik	2015-12-18
\|/
*	Axioms now support the universe binding syntax.	Pierre-Marie Pédrot	2015-10-08
*	STM: Reset takes Ltac <ident> into account (Close #4316)	Enrico Tassi	2015-09-15
*	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
*	Add a [Redirect] vernacular command	Clément Pit--Claudel	2015-05-04
*	STM: if Set Universe Polymorphism then synchronous (#4119)	Enrico Tassi	2015-03-22
*	Reset "section name" works again (Close #3933)	Enrico Tassi	2015-02-15
*	Update headers.	Maxime Dénès	2015-01-12
*	Proof using: New vernacular to name sets of section variables	Enrico Tassi	2014-12-18
*	new: Optimize Proof, Optimize Heap	Enrico Tassi	2014-11-09
*	vernac_classifier: VernacDeclareTacticDefinition does not alter the parser	Enrico Tassi	2014-11-03
*	Add [Info] command.	Arnaud Spiwack	2014-11-01
*	Feedback message: hold extra info to help routing	Enrico Tassi	2014-10-31
*	Notation: option to attach extra pretty printing rules to notations	Enrico Tassi	2014-09-29
*	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot	2014-09-10
*	Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)	Enrico Tassi	2014-09-09
*	Remove [Infer] option of records.	Arnaud Spiwack	2014-09-04
*	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi	2014-08-05
*	STM: Classify Let as non asynchronous (Closes: #3486)	Enrico Tassi	2014-08-05
*	STM: VtQuery holds the id of the state it refers to	Carst Tankink	2014-08-04
*	Add toplevel commands to declare global universes and constraints.	Matthieu Sozeau	2014-07-01
*	Remove the syntax [Vernac1. Vernac2. … Vernacn. ].	Arnaud Spiwack	2014-06-06
*	poly: remove unused attribute to STM nodes and vernac classificaiton	Enrico Tassi	2014-05-15
*	Polymorphic Lemmas are like Defined ones for STM	Enrico Tassi	2014-05-15
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	Cleanup in constr, correct classification of polymorphic defs.	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	Rework handling of universes on top of the STM, allowing for delayed	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot	2014-04-25