coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\
* \|	Clarifying and documenting the UState API.	Pierre-Marie Pédrot	2015-10-17
\| *	Lemmas accept the Local flag.	Pierre-Marie Pédrot	2015-10-17
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Remove -vm flag of coqtop.	Maxime Dénès	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-10
\|\\|
\| *	Code cleaning in VM (with Benjamin).	Maxime Dénès	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
\| *	aux_file: export API to ease writing of a Proof Using annotator.	Enrico Tassi	2015-10-08
\| *	Proof using: let-in policy, optional auto-clear, forward closure*	Enrico Tassi	2015-10-08
\| *	Goptions: new value type: optional string	Enrico Tassi	2015-10-08
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
\|/
*	Univs: fix Show Universes.	Matthieu Sozeau	2015-10-02
*	Univs: fix after rebase (from_ctx/from_env)	Matthieu Sozeau	2015-10-02
*	Univs: fix many evar_map initializations and leaks.	Matthieu Sozeau	2015-10-02
*	Prevent States.intern_state and System.extern_intern from looking up files in...	Guillaume Melquiond	2015-09-29
*	Remove some uses of Loadpath.get_paths.	Guillaume Melquiond	2015-09-29
*	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
*	Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)	Guillaume Melquiond	2015-07-28
*	Assumptions: more informative print for False axiom (Close: #4054)	Enrico Tassi	2015-06-29
*	Reinstall Set Printing Universes option overwritten by Maxime!	Matthieu Sozeau	2015-06-28
*	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
*	Add a Set Dump Bytecode command for debugging purposes.	Maxime Dénès	2015-06-23
*	Remove uses of polymorphic equality from prev. commit	Clément Pit--Claudel	2015-06-22
*	Replace 'try ... with Failure "List.last"' with 'if l <> []'	Clément Pit--Claudel	2015-06-22
*	Guard the List.hd call in [Show Intros]	Clément Pit--Claudel	2015-06-22
*	Flag -test-mode intended to be used for ad-hoc prints in test-suite	Enrico Tassi	2015-05-29
*	Fix bug #4159	Matthieu Sozeau	2015-05-27
*	The Fail command does not catch uncaught exception anomalies anymore.	Pierre-Marie Pédrot	2015-05-18
*	Better error message for non-existent required libraries with a From prefix.	Pierre-Marie Pédrot	2015-05-13
*	STM: process_error_hook set in Vernac where fname is known (fix #4229)	Enrico Tassi	2015-05-12
*	Add a [Redirect] vernacular command	Clément Pit--Claudel	2015-05-04
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Make "Add LoadPath" behave accordingly to its documentation.	Guillaume Melquiond	2015-04-02
*	Display the proper error message when Require fails to find a library.	Guillaume Melquiond	2015-04-02
*	From X Require Y looks for X with absolute path, disregarding -R.	Pierre-Marie Pédrot	2015-04-01
*	Putting the From parameter of the Require command into the AST.	Pierre-Marie Pédrot	2015-03-27
*	Load: don't give anomaly on aborted proofs (Close: #3882)	Enrico Tassi	2015-03-23
*	Do not prepend a "Error:" header when the error is expected by the user.	Guillaume Melquiond	2015-03-05
*	Fixing OCaml 3.12 compilation.	Pierre-Marie Pédrot	2015-02-27
*	Fixing bug #3249.	Pierre-Marie Pédrot	2015-02-27
*	Univs: Fix Check calling the kernel to retype in the wrong environment.	Matthieu Sozeau	2015-02-24
*	Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior	Enrico Tassi	2015-02-14
*	Optimized Import/Export the same way as Require Import/Export was	Hugo Herbelin	2015-02-04
*	Prevent spurious warnings about Arguments.	Guillaume Melquiond	2015-01-29
*	Isolate a function for printing evar sets.	Hugo Herbelin	2015-01-24
*	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12