diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-17 17:46:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-17 17:46:20 +0000 |
| commit | 3c73a7b325dfb0bd7634abd0932674ec96479829 (patch) | |
| tree | 10ba9adb2d34b9ab1bd9baa4427546353c62d64c /tactics | |
| parent | 4bca83aee3bb81949f0c820cc2b438af38ff6f26 (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index ec32c643b..06c4fab6e 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 |