coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing printing of generic arguments of tag "var".	Hugo Herbelin	2016-10-22
*	Revert "unification.ml: fix for bug #4763, unif regression"	Maxime Dénès	2016-10-21
*	Adding dependency of the test-suite subsystems in prerequisite (fixing #5150).	Hugo Herbelin	2016-10-20
*	A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).	Hugo Herbelin	2016-10-20
*	Removing output test for module qualification.	Pierre-Marie Pédrot	2016-10-18
*	Fixing to #3209 (Not_found due to an occur-check cycle).	Hugo Herbelin	2016-10-17
*	Merge PR #310 into v8.5	Pierre-Marie Pédrot	2016-10-17
\|\
\| *	Test for bug #4874.	Pierre-Marie Pédrot	2016-10-17
* \|	Fixing a collision about the meta-variable ".." in recursive notations.	Hugo Herbelin	2016-10-12
* \|	Merge remote-tracking branch 'git/bug5123' into v8.5	Matthieu Sozeau	2016-10-12
\|\ \
\| * \|	Fix test-suite file 5123 to fail in case of regression	Matthieu Sozeau	2016-10-11
\| * \|	Fix bug #5123: mark all shelved evars unresolvable	Matthieu Sozeau	2016-10-11
* \| \|	Fix for bug #4863, update the Proofview's env with	Matthieu Sozeau	2016-10-11
\|/ /
* /	Add test file for #4416.	Maxime Dénès	2016-10-10
\|/
*	evarconv.ml: Fix bug #4529, primproj unfolding	Matthieu Sozeau	2016-10-06
*	unification.ml: fix for bug #4763, unif regression	Matthieu Sozeau	2016-10-06
*	Fixing #4970 (confusion between special "{" and non special "{{" in notations).	Hugo Herbelin	2016-10-03
*	Fix test-suite.	Maxime Dénès	2016-09-30
*	Merge branch '4762' into v8.5	Maxime Dénès	2016-09-30
\|\
\| *	Fix #4762.	Cyprien Mangin	2016-09-30
* \|	Fix a bug in subst releaved by an OCaml warning.	Maxime Dénès	2016-09-29
\|/
*	Fixing #5095 (non relevant too strict test in let-in abstraction).	Hugo Herbelin	2016-09-22
*	Fixing test-suite after commit 43104a0b.	Pierre-Marie Pédrot	2016-09-14
*	Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.	Hugo Herbelin	2016-09-12
*	Test for #5077.	Hugo Herbelin	2016-09-10
*	Test file for #5065 - Anomaly: Not a proof by induction	Maxime Dénès	2016-09-05
*	Fix test-suite after Frédéric's 6231f07b2.	Maxime Dénès	2016-09-01
*	Fix bug #5043: [Admitted] lemmas pick up section variables.	Pierre-Marie Pédrot	2016-08-31
*	Fixing an anomaly in printing a unification error message.	Hugo Herbelin	2016-08-20
*	Fix bug #4673: regression in setoid_rewrite.	Matthieu Sozeau	2016-07-29
*	Fix bug #3886, generation of obligations of fixes	Matthieu Sozeau	2016-07-29
*	Fix #4769, univ poly and elim schemes in sections	Matthieu Sozeau	2016-07-29
*	Fix bug #4754, allow conversion problems to remain	Matthieu Sozeau	2016-07-26
*	Fix bug #4780: universe leak in letin_tac	Matthieu Sozeau	2016-07-20
*	Fix Errors.out missing a dot...	Matthieu Sozeau	2016-07-19
*	Fixing printing of evar name in an error message of instantiate.	Hugo Herbelin	2016-07-13
*	Fix test file for #4858.	Maxime Dénès	2016-07-08
*	Update csdp.cache.	Maxime Dénès	2016-07-08
*	Test file for #4858.	Maxime Dénès	2016-07-08
*	Add test file for #4880.	Maxime Dénès	2016-07-08
*	Update csdp.cache.	Maxime Dénès	2016-07-06
*	Merge remote-tracking branch 'github/pr/199' into v8.5	Maxime Dénès	2016-07-06
\|\
* \|	congruence fix: test-suite code and update CHANGES	Matthieu Sozeau	2016-07-05
* \|	congruence: Restrict refreshing to Set	Matthieu Sozeau	2016-07-04
* \|	congruence/univs: properly refresh (fix #4609)	Matthieu Sozeau	2016-07-04
* \|	test-suite: test checking of libraries checksum.	Maxime Dénès	2016-07-04
* \|	Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).	Hugo Herbelin	2016-07-01
* \|	Univs: allowing notations to take univ instances	Matthieu Sozeau	2016-06-27
* \|	Forbidding silently dropped universes instances in	Matthieu Sozeau	2016-06-27
* \|	More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).	Hugo Herbelin	2016-06-27