coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| *	A hack to fix another regression with Ltac trace report in 8.5. E.g.	Hugo Herbelin	2016-06-18
\| * \|	Set required version of camlp5 to 6.06.	Maxime Dénès	2016-06-17
\|/ /
* \|	par: like all: but in parallel	Enrico Tassi	2016-06-17
* \|	remote counter: avoid thread race on sockets (fix #4823)	Enrico Tassi	2016-06-17
* \|	Mentioning goal selectors in CHANGES	Enrico Tassi	2016-06-17
\| *	remote counter: avoid thread race on sockets (fix #4823)	Enrico Tassi	2016-06-17
* \|	Merge branch 'nzgcd' into trunk	Matthieu Sozeau	2016-06-16
\|\ \
\| * \|	Remove unneded hints in NZGcd	Matthieu Sozeau	2016-06-16
\|/ /
* \|	proof mode: print unification constraints	Matthieu Sozeau	2016-06-16
* \|	Tentative fix of test-suite file to avoid loop	Matthieu Sozeau	2016-06-16
* \|	Typeclasses:rename solve_instantiation* & use Hook	Matthieu Sozeau	2016-06-16
* \|	Fix resolve_one_typeclass to use the new engine	Matthieu Sozeau	2016-06-16
* \|	Bind resolve_one_typeclass to 8.5 or 8.6 resolution	Matthieu Sozeau	2016-06-16
* \|	Fix wrong tabulation in CHANGES	Matthieu Sozeau	2016-06-16
* \|	Put autoapply back, lost during rebase	Matthieu Sozeau	2016-06-16
* \|	Cleanup and refactoring	Matthieu Sozeau	2016-06-16
* \|	Document new Hint Mode option.	Matthieu Sozeau	2016-06-16
* \|	Extend Hint Mode to handle the no-head-evar case	Matthieu Sozeau	2016-06-16
* \|	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
* \|	Example given at DeepSpec workshop	Matthieu Sozeau	2016-06-16
* \|	Purely refactoring and code/API cleanup.	Matthieu Sozeau	2016-06-16
* \|	eauto: fix test-suite file	Matthieu Sozeau	2016-06-16
* \|	bteauto: a Proofview.tactic for multiple goals	Matthieu Sozeau	2016-06-16
* \|	Typeclasses: allow shelved subgoals	Matthieu Sozeau	2016-06-16
* \|	Minor cleanup	Matthieu Sozeau	2016-06-16
* \|	Typeclasses: refine the eauto tactic	Matthieu Sozeau	2016-06-16
* \|	Typeclasses: verbosity and Limit Intros options	Matthieu Sozeau	2016-06-16
* \|	Proofview: extensions for backtracking eauto	Matthieu Sozeau	2016-06-16
* \|	typeclass resolution: add two compatibility options	Matthieu Sozeau	2016-06-16
* \|	setoid_rewrite: fix the Params resolution tactic	Matthieu Sozeau	2016-06-16
* \|	Fix incorrect caching of local hints w.r.t sections	Matthieu Sozeau	2016-06-16
* \|	Compat with ocaml 4.01	Matthieu Sozeau	2016-06-16
* \|	Fix iterative deepening strategy failing too early	Matthieu Sozeau	2016-06-16
* \|	Implement limited proof search and iterative deepening.	Matthieu Sozeau	2016-06-16
* \|	Typeclasses eauto based on new proof engine,	Matthieu Sozeau	2016-06-16
* \|	Typeclasses: stdlib fixes for new search algorithm	Matthieu Sozeau	2016-06-16
* \|	Refine 9cc95f5, unification of Let-In's, bug #3929	Matthieu Sozeau	2016-06-16
* \|	Small factorization in the typing flags of the kernel.	Pierre-Marie Pédrot	2016-06-16
\|\ \
\| * \|	Factorizing the uses of Declareops.safe_flags.	Pierre-Marie Pédrot	2016-06-16
\| * \|	Adding a default safe set of kernel typing flags to Declareops.	Pierre-Marie Pédrot	2016-06-16
\|/ /
* \|	Fixing a mispelling coma -> comma.	Hugo Herbelin	2016-06-16
* \|	Typo in comment.	Hugo Herbelin	2016-06-16
* \|	Fixing space in an error message.	Hugo Herbelin	2016-06-16
* \|	Fixing printing of Register retroknowledge.	Hugo Herbelin	2016-06-16
* \|	Fixing Add Parametric Relation by adding printer for binders.	Hugo Herbelin	2016-06-16
* \|	Adding printers for ring and field commands.	Hugo Herbelin	2016-06-16
* \|	Fixing printing of Function.	Hugo Herbelin	2016-06-16
* \|	Isolating and exporting a function for printing body of a recursive definition.	Hugo Herbelin	2016-06-16
* \|	Simplification in ppvernac.ml.	Hugo Herbelin	2016-06-16
* \|	Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.	Hugo Herbelin	2016-06-16