Abstraction de l'implémentation des signatures de Sign en vue intégration du let-in

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

3 files changed, 22 insertions, 18 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 02d76010cc..15e9069dda 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -590,8 +590,10 @@ let unify_resolve (c,clenv) gls =
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_untyped_hyps <some goal> *)
 
-let make_local_hint_db (lid, ltyp) = 
-  let hintlist = list_map_append2 make_resolve_hyp lid ltyp in
+let make_local_hint_db sign = 
+  let hintlist =
+    list_map_append2 make_resolve_hyp
+      (ids_of_sign sign) (vals_of_sign sign) in
   Hint_db.add_list hintlist Hint_db.empty
 
 
@@ -711,19 +713,19 @@ let decomp_empty_term c gls =
 (* n is the max depth of search *)
 (* local_db contains the local Hypotheses *)
 
-let rec search_gen decomp n db_list local_db add_sign goal =
+let rec search_gen decomp n db_list local_db extra_sign goal =
   if n=0 then error "BOUND 2";
   let decomp_tacs = match decomp with 
     | 0 -> [] 
     | p -> 
-	(tclTRY_sign decomp_empty_term add_sign)
+	(tclTRY_sign decomp_empty_term extra_sign)
 	::
 	(List.map 
 	   (fun id -> tclTHEN (decomp_unary_term (VAR id)) 
 		(tclTHEN 
 		   (clear_one id)
 		   (search_gen decomp p db_list local_db nil_sign)))
-	   (fst (pf_untyped_hyps goal))) 
+	   (ids_of_sign (pf_hyps goal))) 
   in
   let intro_tac = 
     tclTHEN intro 
@@ -736,7 +738,8 @@ let rec search_gen decomp n db_list local_db add_sign goal =
 	   with Failure _ -> [] 
 	 in
          search_gen decomp n db_list
-	   (Hint_db.add_list hintl local_db) ([hid],[htyp]) g') 
+	   (Hint_db.add_list hintl local_db)
+	   (add_sign (hid,htyp) nil_sign) g') 
   in
   let rec_tacs = 
     List.map 
@@ -854,7 +857,7 @@ let compileAutoArg contac = function
                       contac) 
                  else 
 		   tclFAIL)
-	      (fst ctx) (snd ctx)) g)
+	      (ids_of_sign ctx) (vals_of_sign ctx)) g)
   | UsingTDB ->  
       (tclTHEN  
          (Tacticals.tryAllClauses 
@@ -887,10 +890,11 @@ let rec super_search n db_list local_db argl goal =
          (super_search (n-1) db_list local_db argl) argl))) goal
 
 let search_superauto n ids argl g = 
-  let sigma = 
-    ids,
-    (List.map (fun id -> pf_type_of g (pf_global g id)) ids) in   
-  let hyps = (concat_sign (pf_untyped_hyps g) sigma) in
+  let sigma =
+    List.fold_right
+      (fun id -> add_sign (id,pf_type_of g (pf_global g id)))
+      ids nil_sign in
+  let hyps = concat_sign (pf_untyped_hyps g) sigma in
   super_search n [Stringmap.find "core" !searchtable] (make_local_hint_db hyps)
     argl g
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 891f411a18..7b4a9b2cf9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -67,7 +67,7 @@ let tclTRY_sign (tac:constr->tactic) sign gl =
     | [s]     -> tac (VAR(s)) (* added in order to get useful error messages *)
     | (s::sl) -> tclORELSE (tac (VAR(s))) (arec sl) 
   in 
-  arec (fst sign) gl
+  arec (ids_of_sign sign) gl
 
 let tclTRY_HYPS (tac:constr->tactic) gl = 
   tclTRY_sign tac (pf_untyped_hyps gl) gl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4791209298..1997f09bba 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -729,12 +729,12 @@ let dyn_exact cc gl = match cc with
 
 let (assumption:tactic) = fun gl ->
   let concl =  pf_concl gl in 
-  let rec arec = function
-    | ([],[])          -> error "No such assumption"
-    | (s::sl,a::al) -> if pf_conv_x_leq gl a concl then 
-        refine (VAR(s)) gl else arec (sl,al)
-    | _ -> assert false
-  in 
+  let rec arec sign =
+    if isnull_sign sign then error "No such assumption";
+    let (s,a) = hd_sign sign in
+    if pf_conv_x_leq gl a concl then refine (VAR(s)) gl
+    else arec (tl_sign sign)
+  in
   arec (pf_untyped_hyps gl)
 
 let dyn_assumption = function