coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\
\| *	STM: always stock in vio files the first node (state) of a proof	Enrico Tassi	2016-02-10
\| *	STM: not delegate proofs that contain Vernac(Module\|Require\|Import), #4530	Enrico Tassi	2016-02-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| *	Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.	Maxime Dénès	2016-01-15
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-05
\|\\|
\| *	fixup d2b468a, evar normalization is needed	Enrico Tassi	2016-01-04
\| *	par: check if the goal is not ground and fail (fix #4465)	Enrico Tassi	2016-01-04
* \|	Remove some useless module opening.	Guillaume Melquiond	2016-01-02
* \|	CLEANUP: Vernacexpr.vernac_expr	Matej Kosik	2015-12-18
* \|	Specializing the Dyn module to each usecase.	Pierre-Marie Pédrot	2015-12-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico.	Maxime Dénès	2015-11-02
\| *	STM: fix undo into a branch containing side effects	Enrico Tassi	2015-11-02
\| *	STM: never reopen a branch containing side effects	Enrico Tassi	2015-11-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-30
\|\\|
\| *	Add a way to get the right fix_exn in external vernacular commands	Matthieu Sozeau	2015-10-30
\| *	Handle side-effects of Vernacular commands inside proofs better, so that	Matthieu Sozeau	2015-10-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
\| *	Miscellaneous typos, spacing, US spelling in comments or variable names.	Hugo Herbelin	2015-10-18
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-10
\|\\|
\| *	STM: Work around an occasional crash in dot (debug output)	Alec Faithfull	2015-10-09
\| *	STM: Added functions for saving and restoring the internal state	Alec Faithfull	2015-10-09
\| *	STM: Pass exception information to unreachable_state_hook functions	Alec Faithfull	2015-10-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Proof using: let-in policy, optional auto-clear, forward closure*	Enrico Tassi	2015-10-08
\| *	STM: for PIDE based UIs, edit_at requires no Reach.known_state	Enrico Tassi	2015-10-08
\| *	STM: fix backtrace handling	Enrico Tassi	2015-10-08
* \|	Hardening the API of evarmaps.	Pierre-Marie Pédrot	2015-09-26
\|/
*	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
*	STM: save a full state for queries.	Enrico Tassi	2015-09-01
*	STM: make multiple, admitted, nested proofs work (fix #4314)	Enrico Tassi	2015-07-30
*	STM: emit a warning when a QED/Admitted proof contains a nested lemma	Enrico Tassi	2015-07-30
*	STM: fix backtrack in presence of nested, immediate, proofs	Enrico Tassi	2015-07-30
*	STM: remove assertion not being true for nested, immediate, proofs (#4313)	Enrico Tassi	2015-07-30
*	Fixing what seems to be a typo.	Hugo Herbelin	2015-07-29
*	ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix #4308)	Enrico Tassi	2015-07-28
*	STM: fix a "exn with no safe id attached" error on a failing query	Enrico Tassi	2015-07-14
*	STM: states coming from workers have no proof terminators (Close #4246)	Enrico Tassi	2015-06-09
*	STM: silly mistake in jumping back to an old state (Close #4249)	Enrico Tassi	2015-06-09
*	STM: preserve branch name on edit (Close: #4245, #4246)	Enrico Tassi	2015-05-28
*	nice error for Restart outside a proof (Close: #4235)	Enrico Tassi	2015-05-12
*	Add a [Redirect] vernacular command	Clément Pit--Claudel	2015-05-04
*	STM: print trace on "anomaly, no safe id attached"	Enrico Tassi	2015-04-21
*	CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)	Enrico Tassi	2015-04-02
*	STM: refine the notion of "simply a tactic"	Enrico Tassi	2015-03-27
*	STM: change how proof mode switching commands are handled (decl_mode)	Enrico Tassi	2015-03-26
*	STM: avoid processing asynchronously empty proofs (Close: #4134)	Enrico Tassi	2015-03-25
*	STM: if Set Universe Polymorphism then synchronous (#4119)	Enrico Tassi	2015-03-22