coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
*	Print the type-in-type flag in various user-facing functions.	Pierre-Marie Pédrot	2016-06-18
*	Adding a local type-in-type flag in kernel declarations.	Pierre-Marie Pédrot	2016-06-18
*	Test-suite fix to 1744e37 (injection in context).	Hugo Herbelin	2016-06-18
*	Backporting c064fb933 from 8.5 (another regression with Ltac trace report).	Hugo Herbelin	2016-06-18
*	Adding an "as" clause to specialize.	Hugo Herbelin	2016-06-18
*	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
*	Exporting a generic argument induction_arg. As a consequence,	Hugo Herbelin	2016-06-18
*	A cleaning phase around delayed induction arg + exporting force_induction_arg.	Hugo Herbelin	2016-06-18
*	Adding eintros to respect the e- prefix policy.	Hugo Herbelin	2016-06-18
*	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
*	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