coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Mention more fixes in CHANGES before we release pl2.	Maxime Dénès	2016-07-04
*	Revert "Improve the interpretation scope of arguments of an ltac match."	Maxime Dénès	2016-07-04
*	test-suite: test checking of libraries checksum.	Maxime Dénès	2016-07-04
*	Merge remote-tracking branch 'github/pr/228' into v8.5	Maxime Dénès	2016-07-04
\|\
* \|	Fixing use of "Declare Implicit Tactic" in refine.	Hugo Herbelin	2016-07-01
* \|	Fixing #4881 (synchronizing "Declare Implicit Tactic" with backtrack).	Hugo Herbelin	2016-07-01
* \|	Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).	Hugo Herbelin	2016-07-01
\| *	fix coqide double module linking (error on OCaml 4.03)	Gabriel Scherer	2016-06-28
\|/
*	Merge branch 'forhott' into v8.5	Matthieu Sozeau	2016-06-28
\|\
\| *	Univs/CHANGES: #4097 and annotations on notations	Matthieu Sozeau	2016-06-27
\| *	Refine fix for bug #4097, avoid proj expansion	Matthieu Sozeau	2016-06-27
\| *	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
*	Fix bug #4698: CoqIDE error dialogs piling up when coqtop dies.	Pierre-Marie Pédrot	2016-06-27
*	Fix typo.	Guillaume Melquiond	2016-06-23
*	Remove extraction-specific code from the checker.	Guillaume Melquiond	2016-06-23
*	Reference Manual / Extraction: the original example command no longer works w...	Matej Kosik	2016-06-20
*	A hack to fix another regression with Ltac trace report in 8.5. E.g.	Hugo Herbelin	2016-06-18
*	remote counter: avoid thread race on sockets (fix #4823)	Enrico Tassi	2016-06-17
*	Merge branch 'bug4450' into v8.5	Matthieu Sozeau	2016-06-14
\|\
* \	Merge branch 'bug4725' into v8.5	Matthieu Sozeau	2016-06-14
\|\ \
* \| \|	Admitted: fix #4818 return initial stmt and univs	Matthieu Sozeau	2016-06-14
* \| \|	Fix test-suite file, only part 2 is fixed in 8.5	Matthieu Sozeau	2016-06-13
* \| \|	Univs: fix for part #2 of bug #4816.	Matthieu Sozeau	2016-06-13
* \| \|	evar_conv: Refine occur_rigidly	Matthieu Sozeau	2016-06-13
* \| \|	Tentatively fixing misguiding error message with "binder" type in	Hugo Herbelin	2016-06-13
* \| \|	Minor simplification in evarconv.	Hugo Herbelin	2016-06-12
* \| \|	Another fix to #4782 (a typing error not captured when dealing with bindings).	Hugo Herbelin	2016-06-12
* \| \|	Reserve exception "ConversionFailed" in unification for failure of	Hugo Herbelin	2016-06-12
* \| \|	Protecting eta-expansion in evarconv.ml against ill-typed problems.	Hugo Herbelin	2016-06-12
* \| \|	Fixing bug in printing CannotSolveConstraint (collision of context names).	Hugo Herbelin	2016-06-12
* \| \|	Fixing #4782 (a typing error not captured when dealing with bindings).	Hugo Herbelin	2016-06-11
* \| \|	Fixing a try with in apply that has become too weak in 8.5.	Hugo Herbelin	2016-06-11
* \| \|	Reporting about a few bug fixes (to be continued).	Hugo Herbelin	2016-06-09
* \| \|	Fixing #4644 (regression of unification on evar-evar problems with a match).	Hugo Herbelin	2016-06-09
* \| \|	Minor simplification in evarconv.ml.	Hugo Herbelin	2016-06-09
* \| \|	New update on how to find camlp5 binary and library at configure time.	Hugo Herbelin	2016-06-09
* \| \|	Improve the interpretation scope of arguments of an ltac match.	Hugo Herbelin	2016-06-09
* \| \|	Reverting dbdff037 which does not seem to prevent to have #3638 fixed	Hugo Herbelin	2016-06-09
\| \| *	Univs/(e)auto: fix bug #4450 polymorphic exact hints	Matthieu Sozeau	2016-06-09
\| \|/ \|/\|
* \|	Remove failure on non-.v files (bug #4752).	Guillaume Melquiond	2016-06-09
* \|	Fix bug #4777: Printing time is impacted by large terms that don't print.	Pierre-Marie Pédrot	2016-06-07
* \|	Do not use COQLIBS for the validate rule produced by coq_makefile (bug #4693).	Guillaume Melquiond	2016-06-07
* \|	Fixing problems introduced in 8.5 with Ltac trace report. E.g.	Hugo Herbelin	2016-06-06
* \|	Fix incorrect checking of library checksums.	Maxime Dénès	2016-06-05
* \|	Add license text to the windows installation	Enrico Tassi	2016-06-03
* \|	Fix proof terminators not being detected in presence of curly brackets (bug #...	Guillaume Melquiond	2016-06-03
* \|	Make "coqdoc -g --parse-comments" behave properly (bug #4773).	Guillaume Melquiond	2016-06-03
* \|	Fix build (use the same mllib file as in trunk).	Guillaume Melquiond	2016-06-02