coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin	2018-03-30
\|
*	Fix (partial) #4878: option to stop autodeclaring axiom as instance.	Gaëtan Gilbert	2017-11-28
\|
*	Fix typeclasses eauto shelving.	Théo Zimmermann	2016-11-30
\| \| \| \| \| \| \|	A file in the test-suite had to be modified. It was supposed to reproduce a behavior in intuistionistic-nuprl but it did not really. This commit is not supposed to break intuistionistic-nuprl.
*	Revert more of a477dc for good measure	Matthieu Sozeau	2016-11-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We stop failing automatically on non-declared-class nested or toplevel subgoals as in 8.5, instead of the previous a477dc behavior of shelving those goals and failing if shelved goals remained at the end of resolution. It means typeclass resolution during refinement is closer to all:typeclasses eauto. Hints in typeclass_instances for non-declared classes can be used during resolution of _nested_ subgoals when it is fired from type-inference, toplevel goals considered in this case are still only classes (as in 8.5 and before). The code that triggers the restriction to only declared class subgoals is commented. Revert changes to test-suite, adding test for #5203, #5198 is fixed too. Add corresponding tests in the test-suite (that will break if we, e.g. disallow non-class subgoals) and update the refman accordingly.
*	Revert part of a477dc, disallow_shelved	Matthieu Sozeau	2016-11-15
\| \| \| \| \| \| \| \| \|	In only_classes mode we do not try to implement a stricter semantics for shelved goals in 8.6. Leaving this for 8.7. Update the documentation as well. Remove a spurious printf call as well. Fix test-suite now that shelved goals are allowed
*	typeclasses eauto Implem/doc of shelving strategy	Matthieu Sozeau	2016-11-03
\| \| \| \| \| \|	Now [typeclasses eauto] mimicks what happens during resolution faithfully, and the shelving behavior/requirements for a successful proof-search are documented.
*	Fix handling of only_classes at toplevel	Matthieu Sozeau	2016-11-03
\|
*	Test new syntax for hints and typeclass options	Matthieu Sozeau	2016-11-03
\|
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
\|\
* \|	Purely refactoring and code/API cleanup.	Matthieu Sozeau	2016-06-16
\| \| \| \| \| \| \| \|	Fix test-suite files
* \|	bteauto: a Proofview.tactic for multiple goals	Matthieu Sozeau	2016-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Add an option to force backtracking at toplevel, which is used by default when calling typeclasses eauto on a set of goals. They might be depended on by other subgoals, so the tactic should be backtracking by default, a once can make it not backtrack.
* \|	Implement limited proof search and iterative deepening.	Matthieu Sozeau	2016-06-16
\| \| \| \| \| \| \| \|	Fix typo in proofview
* \|	Add an Iterative Deepening search strategy to typeclass resolution.	Matthieu Sozeau	2015-07-27
\|/
*	test-suite: fix success/Typeclasses.v	glondu	2010-10-05
\| \| \| \| \| \|	Obviously broken since r13359 (remove native Π)... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13502 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Substitute terms for evars-as-goals as soon as they are solved in	msozeau	2009-11-27
	typeclass resolution. Fixes a bug reported by Eelis van der Weegen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12545 85f007b7-540e-0410-9357-904b9bb8a0f7