coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-06-29	[test-suite] async-proofs off in tests with Fail Timeout	Enrico Tassi
	Apparently the `Timeout` exception is raised by a signal handled, and that can happen when the running thread is a worker manager, rather than the main thread (the one that should be interrupted). Given that the point of these tests is to test *auto and not the STM, we disable async proofs forcibly.
2019-01-24	Make `Instance` without a body always open a proof.	Maxime Dénès

2017-11-28	Fix (partial) #4878: option to stop autodeclaring axiom as instance.	Gaëtan Gilbert

2016-11-16	Revert more of a477dc for good measure	Matthieu Sozeau
	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.
2016-11-15	Revert part of a477dc, disallow_shelved	Matthieu Sozeau
	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
2016-11-03	Fix test-suite files relying on tcs bugs	Matthieu Sozeau
	- One was expecting shelved goals to remain after resolution (from refine). - The other too were relying on the wrong classification of subgoals as typeclass subgoals at toplevel.
2016-11-03	typeclasses eauto Implem/doc of shelving strategy	Matthieu Sozeau
	Now [typeclasses eauto] mimicks what happens during resolution faithfully, and the shelving behavior/requirements for a successful proof-search are documented.
2016-09-28	Typeclass backtracking example by J. Leivant	Matthieu Sozeau

2016-06-16	Tentative fix of test-suite file to avoid loop	Matthieu Sozeau
	Looping on jenkins only, couldn't reproduce locally. To be investigated further.
2016-06-16	Cleanup and refactoring	Matthieu Sozeau

2016-06-16	Revise syntax of Hint Cut	Matthieu Sozeau
	As noticed by C. Cohen it was confusingly different from standard notation.
2016-06-16	Example given at DeepSpec workshop	Matthieu Sozeau

2016-06-16	Purely refactoring and code/API cleanup.	Matthieu Sozeau
	Fix test-suite files
2016-06-16	bteauto: a Proofview.tactic for multiple goals	Matthieu Sozeau
	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.