coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove a failwith ""	Gaëtan Gilbert	2017-09-29
*	Remove unused Failure catch	Gaëtan Gilbert	2017-09-29
*	Remove TODO comment (Evar.t is opaque)	Gaëtan Gilbert	2017-09-29
*	Cleanup suggest_bullet	Gaëtan Gilbert	2017-09-29
*	Typo in coqdep man	Gaëtan Gilbert	2017-09-29
*	Remove some duplication between Typeops and Nativenorm.	Gaëtan Gilbert	2017-09-29
*	Remove trivial TODO comment (constants can't be template poly now).	Gaëtan Gilbert	2017-09-28
*	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\
* \	Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...	Maxime Dénès	2017-09-25
\|\ \
* \ \	Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ...	Maxime Dénès	2017-09-25
\|\ \ \
* \ \ \	Merge PR #1079: Avoid generated names for html pages of the reference manual ...	Maxime Dénès	2017-09-25
\|\ \ \ \
* \ \ \ \	Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...	Maxime Dénès	2017-09-25
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #1057: Reporting locations in error messages about notation formats.	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #1060: An optimization of tactic constructor	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #1075: Re-enable checker error messages	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \|	Discharge.ml: cosmetic renaming of some variables.	Hugo Herbelin	2017-09-23
\| \| \| \| \| \| \| * \|	Fixing #5755 (discharging of inductive types not correct with let-ins).	Hugo Herbelin	2017-09-23
\| \|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).	Hugo Herbelin	2017-09-23
\| \| \| \| \| \| * \|	Fixing _rect bug for inductive types with let-ins and non-rec uniform params.	Hugo Herbelin	2017-09-23
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
\| \| \| \| \| * \|	Avoid generated names for html pages of the reference manual (bug #4742).	Guillaume Melquiond	2017-09-22
\| \|_\|_\|_\|/ / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #1055: Remove STM vernaculars	Maxime Dénès	2017-09-22
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as exp...	Maxime Dénès	2017-09-22
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a contex...	Maxime Dénès	2017-09-22
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #1071: Mark "Set Tactic Compat Context" as deprecated.	Maxime Dénès	2017-09-22
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #1070: Remove remaining occurrences of -just-parsing.	Maxime Dénès	2017-09-22
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdir	Maxime Dénès	2017-09-22
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #1063: [flags] Flag `open Flags`	Maxime Dénès	2017-09-22
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1061: Fix appveyor build	Maxime Dénès	2017-09-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \| \| \|	Fix -silent flag of coqchk after ff918e4.	Maxime Dénès	2017-09-21
\| \| \| \| \| \| \| \| \| * \| \| \| \|	Adapt checker to change in locations.	Maxime Dénès	2017-09-21
\| \| \| \| \| \| * \| \| \| \| \| \| \|	Proposing meta names more distinguishable from evar names than ?M42.	Hugo Herbelin	2017-09-21
\| \| \| \| \| \| * \| \| \| \| \| \| \|	A possible fix to BZ#5750 (ability to print context of ltac subterm match).	Hugo Herbelin	2017-09-21
\| \| \| \| \| \| \| \|_\|_\|_\|_\|/ / \| \| \| \| \| \| \|/\| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \|	[checker] Add missing Feedback printer (BZ#5587)	Emilio Jesus Gallego Arias	2017-09-21
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Do not reinstall preinstalled packages under AppVeyor.	Maxime Dénès	2017-09-21
\| * \| \| \| \| \| \| \| \| \| \|	Print Cygwin setup output rather than logging in to a file.	Maxime Dénès	2017-09-21
\|/ / / / / / / / / / /
\| \| \| \| * / / / / / /	Mark "Set Tactic Compat Context" as deprecated.	Guillaume Melquiond	2017-09-21
\| \|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \|	Remove remaining occurrences of -just-parsing.	Guillaume Melquiond	2017-09-21
\| \|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \|	In gitlab set TRAVIS_BRANCH so user overlays will work as expected.	Gaëtan Gilbert	2017-09-20
\| \|_\|_\|/ / / / / \|/\| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	coq_makefile: dont show errors from failed (ignored) rmdir	Ralf Jung	2017-09-20
\| \|/ / / / / / \|/\| \| \| \| \| \|
\| * \| \| \| \| \|	[flags] Flag `open Flags`	Emilio Jesus Gallego Arias	2017-09-20
\|/ / / / / /
\| \| \| * / /	An optimization of tactic constructor.	Hugo Herbelin	2017-09-19
\| \| \|/ / / \| \|/\| \| \|
* \| \| \| \|	Merge PR #1036: Unify EConstr.t equality	Maxime Dénès	2017-09-19
\|\ \ \ \ \ \| \|/ / / / \|/\| \| \| \|
\| \| * \| \|	Improve documentation of Status message.	Maxime Dénès	2017-09-19
\| \| * \| \|	Remove STM vernaculars.	Maxime Dénès	2017-09-19
\| \| * \| \|	Add XML protocol support for Wait.	Maxime Dénès	2017-09-19
* \| \| \| \|	Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).	Maxime Dénès	2017-09-19
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #1043: Disable OSX signing for temporary artifacts.	Maxime Dénès	2017-09-19
\|\ \ \ \ \ \
\| \| \| \| \| \| *	Document UState.universe_context.	Gaëtan Gilbert	2017-09-19
\| \| \| \| \| \| *	Don't lose names in UState.universe_context.	Gaëtan Gilbert	2017-09-19
\| \| \| \| \| \| *	test-suite: polymorphism	Matthieu Sozeau	2017-09-19