coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Stronger static invariant in equality upto universes.	Pierre-Marie Pédrot	2016-10-31
*	Moving Universes to the engine/ folder.	Pierre-Marie Pédrot	2016-10-30
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\
\| *	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
\| \| \|\ \
* \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\\| \| \| \|
\| \| * \| \|	Remove incorrect assertion in cbn (bug #4822).	Guillaume Melquiond	2016-10-22
\| \| \| * \|	Fix a bug in error printing of unif constraints	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.6'	Pierre-Marie Pédrot	2016-10-18
\|\\| \| \|
\| * \| \|	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
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\\| \|
\| * \|	Completing reverting generalization and cleaning of the return clause inference.	Hugo Herbelin	2016-10-13
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\\| \|
\| * \|	Reverting generalization and cleaning of the return clause inference in v8.6.	Hugo Herbelin	2016-10-11
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\| \|
\| * \|	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
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\| \|
\| * \|	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
\| \|\ \
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\| \| \|
\| * \| \|	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
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-27
\|\\| \| \|
\| * \| \|	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
\| * \| \|	Inference of return clause: giving uniformly priority to "small inversion".	Hugo Herbelin	2016-09-26
\| * \| \|	Fix bug #5096: [vm_compute] is exponentially slower than [native_compute].	Pierre-Marie Pédrot	2016-09-23
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-23
\|\\| \| \|
\| * \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-23
\| \|\ \ \ \| \| \| \|/ \| \| \|/\|
\| \| * \|	Fixing #5095 (non relevant too strict test in let-in abstraction).	Hugo Herbelin	2016-09-22
* \| \| \|	Make the Coq codebase independent from Ltac-related code.	Pierre-Marie Pédrot	2016-09-16
\|\ \ \ \
\| * \| \| \|	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
* \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\ \ \ \ \ \| \| \|/ / / \| \|/\| \| \|
\| * \| \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-14
\| \|\ \ \ \ \| \| \| \|/ / \| \| \|/\| \|