A slightly more efficient test of well-typedness of restriction of

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

0 files changed, 0 insertions, 0 deletions