coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
*	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
*	Specializing the Dyn module to each usecase.	Pierre-Marie Pédrot	2015-12-04
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\
\| *	vio: fix argument parsing (progress on #4442)	Enrico Tassi	2015-12-01
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: correctly register universe binders for lemmas.	Matthieu Sozeau	2015-11-28
* \|	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-29
\|\\|
\| *	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
* \|	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
* \|	Clarifying and documenting the UState API.	Pierre-Marie Pédrot	2015-10-17
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	When typechecking a lemma statement, try to resolve typeclasses before	Matthieu Sozeau	2015-10-14
* \|	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
\| *	TQueue: Allow some tasks to be saved when clearing a TQueue	Alec Faithfull	2015-10-09
\| *	TQueue: Expose the length of TQueues	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
\|\\|
\| *	Axioms now support the universe binding syntax.	Pierre-Marie Pédrot	2015-10-08
\| *	Proof using: let-in policy, optional auto-clear, forward closure*	Enrico Tassi	2015-10-08
\| *	Spawn: use each socket exclusively for writing or reading	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
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\ \
\| \| *	Univs: fix semantics of Type in proof mode in universe-polymorphic mode	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix handling of side effects/delayed proofs	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix many evar_map initializations and leaks.	Matthieu Sozeau	2015-10-02
\| \|/
\| *	Remove some uses of Loadpath.get_paths.	Guillaume Melquiond	2015-09-29
* \|	Hardening the API of evarmaps.	Pierre-Marie Pédrot	2015-09-26
* \|	Rich printing of messages.	Pierre-Marie Pédrot	2015-09-20
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\\|
\| *	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
* \|	More potentialities in proof_terminators.	Pierre-Marie Pédrot	2015-09-08
* \|	Opacifying the proof_terminator type.	Pierre-Marie Pédrot	2015-09-08
\|/
*	STM: save a full state for queries.	Enrico Tassi	2015-09-01
*	Removing code duplication in Lemmas.	Pierre-Marie Pédrot	2015-08-19