coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\
* \|	Using monotonic types for conversion functions.	Pierre-Marie Pédrot	2016-02-15
\| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	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
*	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