From 3c73a7b325dfb0bd7634abd0932674ec96479829 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 17 Apr 2010 17:46:20 +0000
Subject: 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
---
 tactics/auto.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index ec32c643b5..06c4fab6e1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -764,15 +764,19 @@ let auto_unif_flags = {
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
+let h_clenv_refine ev c clenv =
+  Refiner.abstract_tactic (TacApply (true,ev,[c,NoBindings],None))
+    (Clenvtac.clenv_refine ev clenv)
+
 let unify_resolve_nodelta (c,clenv) gl =
   let clenv' = connect_clenv gl clenv in
-  let _ = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gl in
-  h_simplest_apply c gl
+  let clenv'' = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gl in
+  h_clenv_refine false c clenv'' gl
 
 let unify_resolve flags (c,clenv) gl =
   let clenv' = connect_clenv gl clenv in
-  let _ = clenv_unique_resolver false ~flags clenv' gl in
-  h_apply true false [dummy_loc,(c,NoBindings)] gl
+  let clenv'' = clenv_unique_resolver false ~flags clenv' gl in
+  h_clenv_refine false c clenv'' gl
 
 let unify_resolve_gen = function
   | None -> unify_resolve_nodelta
-- 
cgit v1.2.3