coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[stm] Remove VtBack from public classification.	Emilio Jesus Gallego Arias	2017-10-17
*	[stm] First step to move interpretation of Undo commands out of the classifier.	Emilio Jesus Gallego Arias	2017-10-17
*	Remove STM vernaculars.	Maxime Dénès	2017-09-19
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	[vernac] Remove stale bool parameter from `VernacStartTheoremProof`	Emilio Jesus Gallego Arias	2017-06-21
*	Merge PR#774: [ide] Add route_id parameter to query call.	Maxime Dénès	2017-06-20
\|\
\| *	[ide] Add route_id parameter to query call.	Emilio Jesus Gallego Arias	2017-06-18
* \|	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
\|/
*	Merge PR#717: [proof] Deprecate "proof mode" API	Maxime Dénès	2017-06-07
\|\
* \|	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
\| *	[proof] Deprecate "proof mode" API	Emilio Jesus Gallego Arias	2017-05-31
\|/
*	Remove VernacError	Gaetan Gilbert	2017-04-21
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\
\| *	Fix anomaly when doing [all:Check _.] during a proof.	Gaetan Gilbert	2017-04-14
* \|	[stm] Remove some obsolete vernacs/classification.	Emilio Jesus Gallego Arias	2017-03-24
\| *	Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"	Maxime Dénès	2016-11-18
\| *	[stm] Remove STM-related vernaculars	Emilio Jesus Gallego Arias	2016-11-17
\|/
*	Add command 'Set foo Append "bar"' for appending to an option (bug #5109).	Guillaume Melquiond	2016-10-01
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	par: like all: but in parallel	Enrico Tassi	2016-06-17
*	Documentation	Enrico Tassi	2016-06-07
*	STM: proof block detection for bullets and { block }	Enrico Tassi	2016-06-06
*	STM: proof block detection/error resilience API	Enrico Tassi	2016-06-06
*	Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"	Enrico Tassi	2016-05-10
*	Moving the Ltac definition command to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
*	Moving Tactic Notation to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
*	Moving VernacSolve to an EXTEND-based definition.	Pierre-Marie Pédrot	2016-03-19
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Remove useless recursive flags.	Guillaume Melquiond	2016-01-01
* \|	CLEANUP: Vernacexpr.VernacDeclareTacticDefinition	Matej Kosik	2015-12-18
* \|	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