- Allow to set a particular transparent_state for the local hint

  database
- Fix [specialize] to properly resolve typeclass constraints.


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

5 files changed, 29 insertions, 17 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index d03c527f4f..b48e8fbc81 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -878,9 +878,12 @@ 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
 
-let make_local_hint_db eapply lems gl =
+let make_local_hint_db ?ts eapply lems gl =
   let sign = pf_hyps gl in
-  let ts = Hint_db.transparent_state (searchtable_map "core") in
+  let ts = match ts with
+    | None -> Hint_db.transparent_state (searchtable_map "core") 
+    | Some ts -> ts
+  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 ts false)) gl
diff --git a/tactics/auto.mli b/tactics/auto.mli
index cd8808bff2..1bc321c940 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -170,7 +170,7 @@ val set_extern_subst_tactic :
    Useful to take the current goal hypotheses as hints;
    Boolean tells if lemmas with evars are allowed *)
 
-val make_local_hint_db : bool -> open_constr list -> goal sigma -> hint_db
+val make_local_hint_db : ?ts:transparent_state -> bool -> open_constr list -> goal sigma -> hint_db
 
 val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 3551b75e52..71bae61eef 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -464,14 +464,18 @@ let evar_dependencies evm p =
     evm ()
 
 let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
+  let nc, gl, subst = Evarutil.push_rel_context_to_named_context env gl in
   let (gl,t,sigma) = 
-    Goal.V82.mk_goal sigma (Environ.named_context_val env) gl Store.empty in
+    Goal.V82.mk_goal sigma nc gl Store.empty in
   let gls = { it = gl ; sigma = sigma } in
   let hints = searchtable_map typeclasses_db in
-  let gls' = eauto ~st:(Hint_db.transparent_state hints) [hints] gls in
+  let gls' =  eauto ~st:(Hint_db.transparent_state hints) [hints] gls in
   let evd = sig_sig gls' in
-  let term = Evarutil.nf_evar evd t in
-  evd, term
+  let t' = let (ev, inst) = destEvar t in
+    mkEvar (ev, Array.of_list subst)
+  in
+  let term = Evarutil.nf_evar evd t' in
+    evd, term
 
 let _ =
   Typeclasses.solve_instanciation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index ed8da10a08..59e7fcca15 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -291,7 +291,7 @@ let e_breadth_search debug n db_list local_db gl =
   with Not_found -> error "eauto: breadth first search failed."
 
 let e_search_auto debug (in_depth,p) lems db_list gl =
-  let local_db = make_local_hint_db true lems gl in
+  let local_db = make_local_hint_db ~ts:full_transparent_state true lems gl in
   if in_depth then
     e_depth_search debug p db_list local_db gl
   else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ab04ebaf61..0ad64c21ca 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1112,11 +1112,14 @@ let rec intros_clearing = function
 (* Modifying/Adding an hypothesis  *)
 
 let specialize mopt (c,lbind) g =
-  let term =
-    if lbind = NoBindings then c
+  let tac, term =
+    if lbind = NoBindings then 
+      let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in
+	tclEVARS evd, nf_evar evd c
     else
       let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
-      let clause = clenv_unify_meta_types clause in
+      let flags = { default_unify_flags with resolve_evars = true } in
+      let clause = clenv_unify_meta_types ~flags clause in
       let (thd,tstack) = whd_stack clause.evd (clenv_value clause) in
       let nargs = List.length tstack in
       let tstack = match mopt with
@@ -1133,16 +1136,18 @@ let specialize mopt (c,lbind) g =
 	errorlabstrm "" (str "Cannot infer an instance for " ++
           pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++
 	  str ".");
-      term
+       tclEVARS clause.evd, term
   in
   match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with
        | Var id when List.mem id (pf_ids_of_hyps g) ->
-	     tclTHENFIRST
+	   tclTHEN tac
+	     (tclTHENFIRST
 	       (fun g -> internal_cut_replace id (pf_type_of g term) g)
-	       (exact_no_check term) g
-       | _ -> tclTHENLAST
-                 (fun g -> cut (pf_type_of g term) g)
-                 (exact_no_check term) g
+	       (exact_no_check term)) g
+       | _ -> tclTHEN tac
+	   (tclTHENLAST
+              (fun g -> cut (pf_type_of g term) g)
+              (exact_no_check term)) g
 
 (* Keeping only a few hypotheses *)