coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin	2018-03-30
\|
*	Fixing test #2830.	Pierre-Marie Pédrot	2015-02-23
\|
*	Revert "Adapting two files from test-suite to now forbidden Require's in ↵	Maxime Dénès	2015-01-17
\| \| \| \| \| \|	modules." This reverts commit b0fceb96d0aaa2db6e774c629503be459017608e.
*	Fixing test for bug #2830.	Pierre-Marie Pédrot	2015-01-06
\|
*	Adapting two files from test-suite to now forbidden Require's in modules.	Hugo Herbelin	2015-01-04
\| \| \| \| \|	Status of 335 and 3363 which are explicitly testing Require in modules still to be addressed (to remove from test suite?).
*	Completing test for bug report #2830	Hugo Herbelin	2014-06-30
\|
*	A slightly more efficient test of well-typedness of restriction of	herbelin	2013-02-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
*	Fixing one part of #2830 (anomaly "defined twice" due to nested calls to	herbelin	2013-01-28
	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