coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-10-04	rename test files (do not start by a digit)	Vincent Laporte

2018-03-30	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin

2015-02-23	Fixing test #2830.	Pierre-Marie Pédrot

2015-01-17	Revert "Adapting two files from test-suite to now forbidden Require's in ↵	Maxime Dénès
	modules." This reverts commit b0fceb96d0aaa2db6e774c629503be459017608e.
2015-01-06	Fixing test for bug #2830.	Pierre-Marie Pédrot

2015-01-04	Adapting two files from test-suite to now forbidden Require's in modules.	Hugo Herbelin
	Status of 335 and 3363 which are explicitly testing Require in modules still to be addressed (to remove from test suite?).
2014-06-30	Completing test for bug report #2830	Hugo Herbelin

2013-02-21	A slightly more efficient test of well-typedness of restriction of	herbelin
	evars (though this might be slighty more costly). This incidentally solves Appel's part of bug #2830 even though a conceptual problem around the interaction of unification with the proof engine has to be solved. Indeed, what to do when unification, called as part of a tactic, solves or refines the current goal by side effect. Somehow, unifyTerms or tclEVARS should take this possibility into consideration, either by forbidding the refinement of the current goal by side effect, or by acknowledging this refinement by producing new subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16232 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28	Fixing one part of #2830 (anomaly "defined twice" due to nested calls to	herbelin
	the function solve_candidates introduced in 8.4). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16163 85f007b7-540e-0410-9357-904b9bb8a0f7