coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Clean up type classes flags and update compat file.	Maxime Dénès	2016-10-05
*	Fix bug #4893: not_evar: unexpected failure in 8.5pl1.	Pierre-Marie Pédrot	2016-08-30
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	Typeclasses: fix treatment of exceptions in compat	Matthieu Sozeau	2016-06-27
*	Typeclasses: mark unresolvable goals in new implementation	Matthieu Sozeau	2016-06-27
*	We want tclORELSE to catch exceptions on backtrackings	Matthieu Sozeau	2016-06-27
*	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
*	Put autoapply back, lost during rebase	Matthieu Sozeau	2016-06-16
*	Cleanup and refactoring	Matthieu Sozeau	2016-06-16
*	Purely refactoring and code/API cleanup.	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
*	typeclass resolution: add two compatibility options	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
*	Add a synonymous Set Debug Typeclasses for Set Typeclasses Debug, for uniform...	Hugo Herbelin	2016-06-02
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Put the "exact" family of tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Moving Eauto and Class_tactics to tactics/.	Pierre-Marie Pédrot	2016-03-25
*	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21
*	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\
* \|	Moving conversion functions to the new tactic API.	Pierre-Marie Pédrot	2016-02-15
\| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \|	Inlining the only use of Clenv.connect_clenv.	Pierre-Marie Pédrot	2015-11-18
* \|	Indexing Proofview.goals with a stage.	Pierre-Marie Pédrot	2015-10-20
* \|	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
\| *	Generalize fix for auto from PMP to eauto and typeclasses eauto.	Matthieu Sozeau	2015-10-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Exporting the original unprocessed hint in the hint running function.	Pierre-Marie Pédrot	2015-10-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-06
\|\\|
\| *	Fix bug #4354: interpret hints in the right env and sigma.	Matthieu Sozeau	2015-10-06
* \|	Add an Iterative Deepening search strategy to typeclass resolution.	Matthieu Sozeau	2015-07-27
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-02
\|\\|
\| *	class_tactics: make interruptible	Enrico Tassi	2015-06-29
\| *	class_tactics: remove catch-all, use Errors.noncritical	Enrico Tassi	2015-06-29
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13