Solved a few problems of auto by bypassing the call to apply.

Indeed, calling apply was inefficient (doing again a unification known
to work) and moreover unsound (apply's unification is poorly tunable
and the flags used in the first unification - in clenv_unique_resolve -
were lost for apply).
Solved the problem of still having a pretty acceptable user-friendly
"info auto" by concealing the direct call to "clenv_refine" as a call
to apply.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12948 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions