coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Prevent unsafe overwriting of Required modules by toplevel library.	Maxime Dénès	2016-07-05
* \|	congruence fix: test-suite code and update CHANGES	Matthieu Sozeau	2016-07-05
* \|	Pass .v files to coqc in Makefile produced by coq_makefile (bug #4896).	Guillaume Melquiond	2016-07-05
* \|	Add mailmap entry.	Guillaume Melquiond	2016-07-05
* \|	Bug fix : variable capture in ltac code of Nsatz	thery	2016-07-05
* \|	Merge branch 'congruencefix' into v8.5	Matthieu Sozeau	2016-07-04
\|\ \
\| * \|	congruence: Restrict refreshing to Set	Matthieu Sozeau	2016-07-04
\| * \|	congruence: remove casts of indexed terms	Matthieu Sozeau	2016-07-04
\| * \|	congruence/univs: properly refresh (fix #4609)	Matthieu Sozeau	2016-07-04
* \| \|	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
\| \| \| *	Unbreak singleton list-like notation (-compat 8.4)	Jason Gross	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