coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \|	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
* \|	Documentation by giving a name to a large type.	Pierre-Marie Pédrot	2015-08-19
\| *	Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080	Jason Gross	2015-08-14
\|/
*	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
*	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
*	Splitting the library representation on disk in two.	Pierre-Marie Pédrot	2015-06-24
*	STM: states coming from workers have no proof terminators (Close #4246)	Enrico Tassi	2015-06-09