coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing a line warned unused.	Hugo Herbelin	2017-05-14
*	Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).	Hugo Herbelin	2017-05-01
*	Really fixing #2602 which was wrongly working because of #5487 hiding the cause.	Hugo Herbelin	2017-05-01
*	Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."	Maxime Dénès	2017-04-28
*	Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).	Hugo Herbelin	2017-04-28
*	Fix bug #5377: @? patterns broken.	Pierre-Marie Pédrot	2017-04-20
*	Fixing #5460 (limitation in computing deps in pattern-matching compilation).	Hugo Herbelin	2017-04-08
*	Intern names bound in match patterns	Tej Chajed	2017-03-23
*	Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).	Hugo Herbelin	2017-01-22
*	Merge remote-tracking branch 'github/pr/366' into v8.6	Maxime Dénès	2016-12-04
\|\
\| *	Document changes	Matthieu Sozeau	2016-12-02
* \|	Univs: fix bug #5180	Matthieu Sozeau	2016-11-30
\| *	Fix UGraph.check_eq!	Matthieu Sozeau	2016-11-30
\|/
*	Merge remote-tracking branch 'github/pr/339' into v8.6	Maxime Dénès	2016-11-07
\|\
* \	Merge commit 'e6edb33' into v8.6	Maxime Dénès	2016-11-07
\|\ \
\| * \|	More explicit name for status of unification constraints.	Maxime Dénès	2016-11-07
\| \| *	Lets Hints/Instances take an optional pattern	Matthieu Sozeau	2016-11-03
* \| \|	Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).	Hugo Herbelin	2016-10-29
\| \|/ \|/\|
* \|	Merge remote-tracking branch 'github/pr/337' into v8.6	Maxime Dénès	2016-10-28
\|\ \
\| * \|	Complete overhaul of the Arguments vernacular.	Maxime Dénès	2016-10-27
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-26
\|\ \ \
\| * \ \	Merge remote-tracking branch 'github/pr/333' into v8.5	Maxime Dénès	2016-10-25
\| \|\ \ \
\| * \| \| \|	Remove incorrect assertion in cbn (bug #4822).	Guillaume Melquiond	2016-10-22
\| \| \| \| *	Renamings to avoid confusion deprecating old names	Matthieu Sozeau	2016-10-22
\| \| \| \| *	Unification constraint handling (#4763, #5149)	Matthieu Sozeau	2016-10-22
\| \| * \| \|	Fix a bug in error printing of unif constraints	Matthieu Sozeau	2016-10-22
\| \|/ / /
\| \| \| *	Port fix for bugs 4763, 5149, previously 0b417c12e	Matthieu Sozeau	2016-10-22
\| \|_\|/ \|/\| \|
* \| \|	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-10-21
\|\\| \|
\| * \|	Revert "unification.ml: fix for bug #4763, unif regression"	Maxime Dénès	2016-10-21
\| * \|	A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).	Hugo Herbelin	2016-10-20
* \| \|	Attempt to improve error rendering in pattern-matching compilation (#5142).	Hugo Herbelin	2016-10-19
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-18
\|\\| \|
* \| \|	Quick fix to unification regression #4955.	Hugo Herbelin	2016-10-17
\| \|/ \|/\|
\| *	Fixing to #3209 (Not_found due to an occur-check cycle).	Hugo Herbelin	2016-10-17
\| *	Fixing a missing constraint in consider_remaining_unif_constraints.	Hugo Herbelin	2016-10-17
* \|	Completing reverting generalization and cleaning of the return clause inference.	Hugo Herbelin	2016-10-13
* \|	Reverting generalization and cleaning of the return clause inference in v8.6.	Hugo Herbelin	2016-10-11
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-08
\|\\|
* \|	Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.	Pierre-Marie Pédrot	2016-10-08
* \|	Fix bug #4464: "Anomaly: variable H' unbound. Please report.".	Pierre-Marie Pédrot	2016-10-07
\| *	evarconv.ml: Fix bug #4529, primproj unfolding	Matthieu Sozeau	2016-10-06
\| *	w_merge: Add a comment about the (List.rev evars)	Matthieu Sozeau	2016-10-06
\| *	unification.ml: fix for bug #4763, unif regression	Matthieu Sozeau	2016-10-06
* \|	Quick fix to #4595 (making notations containing "ltac:" unused for printing).	Hugo Herbelin	2016-10-04
* \|	Merge remote-tracking branch 'github/pr/263' into v8.6	Maxime Dénès	2016-10-03
\|\ \
* \| \|	Fix bug #4723 and FIXME in API for solve_by_tac	Matthieu Sozeau	2016-09-28
* \| \|	Remove incorrect assertion in cbn (bug #4822).	Guillaume Melquiond	2016-09-28
* \| \|	Posssible abstractions over goal variables when inferring match return clause.	Hugo Herbelin	2016-09-26
* \| \|	Trying an abstracting dependencies heuristic for the match return clause even...	Hugo Herbelin	2016-09-26
* \| \|	Trying a no-inversion no-dependency heuristic for match return clause.	Hugo Herbelin	2016-09-26