Prise en compte de l'env local dans make_apply_entry

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

3 files changed, 51 insertions, 41 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index aeb0cfb595..dd11121526 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -196,8 +196,8 @@ let make_exact_entry name (c,cty) =
 	(head_of_constr_reference (List.hd (head_constr cty)),
 	   { hname=name; pri=0; pat=None; code=Give_exact c })
 
-let make_apply_entry (eapply,verbose) name (c,cty) =
-  let cty = hnf_constr (Global.env()) Evd.empty cty in
+let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
+  let cty = hnf_constr env sigma cty in
   match kind_of_term cty with
     | IsProd _ ->
         let ce = mk_clenv_from () (c,cty) in
@@ -229,37 +229,38 @@ let make_apply_entry (eapply,verbose) name (c,cty) =
    c is a constr
    cty is the type of constr *)
 
-let make_resolves name eap (c,cty) =
+let make_resolves env sigma name eap (c,cty) =
   let ents = 
     map_succeed 
       (fun f -> f name (c,cty)) 
-      [make_exact_entry; make_apply_entry eap]
+      [make_exact_entry; make_apply_entry env sigma eap]
   in 
   if ents = [] then 
     errorlabstrm "Hint" [< prterm c; 'sPC; 'sTR "cannot be used as a hint" >];
   ents
 
 (* used to add an hypothesis to the local hint database *)
-let make_resolve_hyp (hname,_,htyp) = 
+let make_resolve_hyp env sigma (hname,_,htyp) = 
   try
-    [make_apply_entry (true, Options.is_verbose()) hname
+    [make_apply_entry env sigma (true, Options.is_verbose()) hname
        (mkVar hname, body_of_type htyp)]
   with 
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp"
 
-let add_resolves clist dbnames =
+let add_resolves env sigma clist dbnames =
   List.iter 
     (fun dbname ->
        Lib.add_anonymous_leaf
 	 (inAutoHint
 	    (dbname,
      	     (List.flatten
-		(List.map (fun (name,c) -> 
-			     let env = Global.env() in
-			     let ty = type_of env Evd.empty c in
-			     let verbose = Options.is_verbose() in
-			     make_resolves name (true,verbose) (c,ty)) clist))
+		(List.map
+		   (fun (name,c) -> 
+		      let ty = type_of env sigma c in
+		      let verbose = Options.is_verbose() in
+		      make_resolves env sigma name (true,verbose) (c,ty)) clist
+		))
 	    )))
     dbnames
 
@@ -339,11 +340,12 @@ let _ =
     "HintResolve"
     (function 
        | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_CONSTR c] ->
-	   let c1 = Astterm.interp_constr Evd.empty (Global.env()) c in
+	   let env = Global.env() and sigma = Evd.empty in
+	   let c1 = Astterm.interp_constr sigma env c in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
 		      	 | _ -> bad_vernac_args "HintResolve") l in
-	   fun () -> add_resolves [hintname, c1] dbnames
+	   fun () -> add_resolves env sigma [hintname, c1] dbnames
        | _-> bad_vernac_args "HintResolve" )
    
 let _ = 
@@ -365,6 +367,7 @@ let _ =
        | [VARG_IDENTIFIER idr; VARG_VARGLIST l; VARG_IDENTIFIER c] ->
 	   begin 
 	     try
+	       let env = Global.env() and sigma = Evd.empty in
 	       let trad = Declare.global_reference CCI in
 	       let rectype = destMutInd (trad c) in
 	       let consnames = 
@@ -374,7 +377,7 @@ let _ =
 	       let dbnames = if l = [] then ["core"] else 
 	      	 List.map (function VARG_IDENTIFIER i -> string_of_id i
 			     | _ -> bad_vernac_args "HintConstructors") l in
-    	       fun () -> add_resolves lcons dbnames
+    	       fun () -> add_resolves env sigma lcons dbnames
 	     with Invalid_argument("mind_specif_of_mind") -> 
 	       error ((string_of_id c) ^ " is not an inductive type")
 	   end 
@@ -399,6 +402,7 @@ let _ =
     "HintsResolve"
     (function
        | (VARG_VARGLIST l)::lh ->
+	   let env = Global.env() and sigma = Evd.empty in
  	   let lhints = 
 	     List.map (function
 			 | VARG_IDENTIFIER i -> 
@@ -407,7 +411,7 @@ let _ =
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
 		      	 | _-> bad_vernac_args "HintsResolve") l in
-	   fun () -> add_resolves lhints dbnames
+	   fun () -> add_resolves env sigma lhints dbnames
        | _-> bad_vernac_args "HintsResolve")
     
 let _ = 
@@ -600,9 +604,10 @@ let unify_resolve (c,clenv) gls =
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
 
-let make_local_hint_db sign = 
-  let hintlist = list_map_append make_resolve_hyp sign in
-  Hint_db.add_list hintlist Hint_db.empty
+let make_local_hint_db g = 
+  let sign = pf_hyps g in
+  let hintlist = list_map_append (make_resolve_hyp (pf_env g) (project g)) sign
+  in Hint_db.add_list hintlist Hint_db.empty
 
 
 (**************************************************************************)
@@ -617,8 +622,8 @@ let rec trivial_fail_db db_list local_db gl =
   let intro_tac = 
     tclTHEN intro 
       (fun g'->
-	 let hintl = make_resolve_hyp (pf_last_hyp g') in
-	 trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
+	 let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
+	 in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
   in
   tclFIRST 
     (assumption::intro_tac::
@@ -667,13 +672,13 @@ let trivial dbnames gl =
 	   error ("Trivial: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
-  tclTRY (trivial_fail_db db_list (make_local_hint_db (pf_hyps gl))) gl 
+  tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl 
     
 let full_trivial gl =
   let dbnames = stringmap_dom !searchtable in
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
-  tclTRY (trivial_fail_db db_list (make_local_hint_db (pf_hyps gl))) gl
+  tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl
 
 let dyn_trivial = function
   | []                  -> trivial []
@@ -740,7 +745,8 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	 let (hid,_,htyp as d) = pf_last_hyp g' in
 	 let hintl = 
 	   try 
-	     [make_apply_entry (true,Options.is_verbose()) 
+	     [make_apply_entry (pf_env g') (project g')
+		(true,Options.is_verbose()) 
 		hid (mkVar hid,body_of_type htyp)]
 	   with Failure _ -> [] 
 	 in
@@ -771,7 +777,7 @@ let auto n dbnames gl =
       ("core"::dbnames) 
   in
   let hyps = pf_hyps gl in
-  tclTRY (search n db_list (make_local_hint_db hyps) hyps) gl
+  tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
 
 let default_auto = auto !default_search_depth []
 
@@ -780,7 +786,7 @@ let full_auto n gl =
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
   let hyps = pf_hyps gl in
-  tclTRY (search n db_list (make_local_hint_db hyps) hyps) gl
+  tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
   
 let default_full_auto gl = full_auto !default_search_depth gl
 
@@ -816,7 +822,7 @@ let default_search_decomp = ref 1
 let destruct_auto des_opt n gl = 
   let hyps = pf_hyps gl in
   search_gen des_opt n [searchtable_map "core"] 
-    (make_local_hint_db hyps) hyps gl
+    (make_local_hint_db gl) hyps gl
     
 let dautomatic des_opt n = tclTRY (destruct_auto des_opt n)
 
@@ -882,7 +888,8 @@ let rec super_search n db_list local_db argl goal =
         (fun g -> 
 	   let (hid,_,htyp) = pf_last_hyp g in
 	   let hintl =
-	     make_resolves hid (true,false) (mkVar hid,body_of_type htyp) in
+	     make_resolves (pf_env g) (project g)
+	       hid (true,false) (mkVar hid,body_of_type htyp) in
 	   super_search n db_list (Hint_db.add_list hintl local_db)
 	     argl g))
      ::
@@ -902,9 +909,9 @@ let search_superauto n ids argl g =
 	   (id,Retyping.get_assumption_of (pf_env g) (project g) 
 	      (pf_type_of g (pf_global g id))))
       ids empty_var_context in
-  let hyps = List.append (pf_hyps g) sigma in
-  super_search n [Stringmap.find "core" !searchtable] (make_local_hint_db hyps)
-    argl g
+  let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
+  let db = Hint_db.add_list db0 (make_local_hint_db g) in
+  super_search n [Stringmap.find "core" !searchtable] db argl g
 
 let superauto n ids_add argl  = 
   tclTRY (tclCOMPLETE (search_superauto n ids_add argl))
diff --git a/tactics/auto.mli b/tactics/auto.mli
index b65d2ea218..399176c5bc 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -10,6 +10,8 @@ open Proof_type
 open Tacmach
 open Clenv
 open Pattern
+open Environ
+open Evd
 (*i*)
   
 type auto_tactic = 
@@ -66,7 +68,7 @@ val make_exact_entry :
    [cty] is the type of [hc]. *)
 
 val make_apply_entry :
-  bool * bool -> identifier -> constr * constr
+  env -> 'a evar_map -> bool * bool -> identifier -> constr * constr
       -> constr_label * pri_auto_tactic
 
 (* A constr which is Hint'ed will be:
@@ -77,7 +79,7 @@ val make_apply_entry :
        has missing arguments. *)
 
 val make_resolves :
-  identifier -> bool * bool -> constr * constr -> 
+  env -> 'a evar_map -> identifier -> bool * bool -> constr * constr -> 
     (constr_label * pri_auto_tactic) list
 
 (* [make_resolve_hyp hname htyp].
@@ -85,7 +87,9 @@ val make_resolves :
    Never raises an User_exception;
    If the hyp cannot be used as a Hint, the empty list is returned. *)
 
-val make_resolve_hyp : var_declaration -> (constr_label * pri_auto_tactic) list
+val make_resolve_hyp : 
+  env -> 'a evar_map -> var_declaration ->
+      (constr_label * pri_auto_tactic) list
 
 (* [make_extern name pri pattern tactic_ast] *)
 
@@ -96,7 +100,7 @@ val make_extern :
 (* Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints *)
 
-val make_local_hint_db : var_context -> Hint_db.t
+val make_local_hint_db : goal sigma -> Hint_db.t
 
 val priority : (int * 'a) list -> 'a list
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 93e8e6c3a3..49131d1926 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -144,7 +144,7 @@ let rec e_trivial_fail_db db_list local_db goal =
     (tclTHEN Tactics.intro 
        (function g'->
 	  let d = pf_last_hyp g' in
-	  let hintl = make_resolve_hyp d in
+	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
 	     (Hint_db.add_list hintl local_db) g'))) ::
     (e_trivial_resolve db_list local_db (pf_concl goal)) 
@@ -220,7 +220,8 @@ let rec e_search n db_list local_db lg =
       apply_tac_list
 	(tclTHEN Tactics.intro 
 	   (fun g' -> 		   
-	      let hintl = make_resolve_hyp (pf_last_hyp g') in
+	      let hintl = make_resolve_hyp (pf_env g') (project g') 
+			    (pf_last_hyp g') in
 	      (tactic_list_tactic 
 		 (e_search n db_list
 		    (Hint_db.add_list hintl local_db))) g')) 
@@ -238,9 +239,7 @@ let rec e_search n db_list local_db lg =
     tclIDTAC_list lg
 
 let e_search_auto n db_list gl = 
-  tactic_list_tactic 
-    (e_search n db_list (make_local_hint_db (pf_hyps gl)))
-    gl
+  tactic_list_tactic (e_search n db_list (make_local_hint_db gl)) gl
 
 let eauto n dbnames = 
   let db_list =
@@ -258,7 +257,7 @@ let full_eauto n gl =
   let dbnames = stringmap_dom !searchtable in
   let dbnames =  list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
-  let local_db = make_local_hint_db (pf_hyps gl) in
+  let local_db = make_local_hint_db gl in
   tclTRY (tclCOMPLETE (e_search_auto n db_list)) gl
 
 let default_full_auto gl = full_auto !default_search_depth gl