ported r13340 to trunk

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

2 files changed, 12 insertions, 5 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4cac7faae2..9c58b78016 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -798,11 +798,18 @@ let add_hint_lemmas eapply lems hint_db gl =
     list_map_append (pf_apply make_resolves gl (eapply,true,false) None) lems in
   Hint_db.add_list hintlist' hint_db
 
+
+(* Hints supplied by "using" are considered *before* the goal hyps.
+   This gives the user a (limited) way to control the search space.
+   Note: number of premisses is still the main ordering criterion, so
+   local hyps with fewer premisses are still prefered to user supplied
+   hints with larger number of premisses. (BB) *)
 let make_local_hint_db eapply lems gl =
   let sign = pf_hyps gl in
   let hintlist = list_map_append (pf_apply make_resolve_hyp gl) sign in
-  add_hint_lemmas eapply lems
-    (Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false)) gl
+  Hint_db.add_list hintlist
+    (add_hint_lemmas eapply lems
+     (Hint_db.empty empty_transparent_state false) gl)
 
 (* Serait-ce possible de compiler d'abord la tactique puis de faire la
    substitution sans passer par bdize dont l'objectif est de préparer un
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 94ea43f45d..6bd7bc17fa 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2146,9 +2146,9 @@ and interp_genarg ist gl x =
       match tactic_genarg_level s with
       | Some n ->
           (* Special treatment of tactic arguments *)
-          in_gen (wit_tactic n)
-	    (TacArg(valueIn(VFun(ist.trace,ist.lfun,[],
-				 out_gen (globwit_tactic n) x))))
+          in_gen (wit_tactic n) (out_gen (globwit_tactic n) x)
+(*          in_gen (wit_tactic n)
+	    (TacArg(valueIn(val_interp ist gl (out_gen (globwit_tactic n) x))))*)
       | None ->
           lookup_interp_genarg s ist gl x