ported r13340 to trunk

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

3 files changed, 21 insertions, 10 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 6b764b1d90..2b6261169e 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -535,6 +535,7 @@ let destFLambda clos_fun t =
     | FLambda(n,(na,ty)::tys,b,e) ->
         (na,clos_fun e ty,{norm=Cstr;term=FLambda(n-1,tys,b,subs_lift e)})
     | _ -> assert false
+	(* t must be a FLambda and binding list cannot be empty *)
 
 (* Optimization: do not enclose variables in a closure.
    Makes variable access much faster *)
@@ -769,8 +770,8 @@ let rec reloc_rargs_rec depth stk =
 let reloc_rargs depth stk =
   if depth = 0 then stk else reloc_rargs_rec depth stk
 
-let rec drop_parameters depth n stk =
-  match stk with
+let rec drop_parameters depth n argstk =
+  match argstk with
       Zapp args::s ->
         let q = Array.length args in
         if n > q then drop_parameters depth (n-q) s
@@ -779,9 +780,12 @@ let rec drop_parameters depth n stk =
           let aft = Array.sub args n (q-n) in
           reloc_rargs depth (append_stack aft s)
     | Zshift(k)::s -> drop_parameters (depth-k) n s
-    | [] -> assert (n=0); []
-    | _ -> assert false (* we know that n < stack_args_size(stk) *)
-
+    | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
+	if n=0 then []
+	else anomaly
+	  "ill-typed term: found a match on a partially applied constructor"
+    | _ -> assert false
+	(* strip_update_shift_app only produces Zapp and Zshift items *)
 
 (* Iota reduction: expansion of a fixpoint.
  * Given a fixpoint and a substitution, returns the corresponding
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