coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
\|/ / / /
* \| \| \|	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
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\| \| \|
\| * \| \|	Fix [Polymorphic Hint Rewrite].	Matthieu Sozeau	2015-11-27
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-26
\|\\| \| \|
\| * \| \|	Fix output of universe arcs. (Fix bug #4422)	Guillaume Melquiond	2015-11-23
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\| \| \|
\| * \| \|	Adding syntax "Show id" to show goal named id (shelved or not).	Hugo Herbelin	2015-11-02
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\| \| \|
\| * \| \|	Univs: local names handling.	Matthieu Sozeau	2015-10-28
\| * \| \|	Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names	Matthieu Sozeau	2015-10-27
* \| \| \|	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
\| \| *	Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...	Arnaud Spiwack	2015-09-25
* \| \|	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
\| * \|	Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080	Jason Gross	2015-08-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 corresponding field in `VernacInductive`.	Arnaud Spiwack	2015-06-24
\|/
*	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