- Use transparency information all the way through unification and

conversion.
- Fix trans_fconv* to use evars correctly.
- Normalize the goal with respect to evars before rewriting in
[rewrite], allowing to see instanciations from other subgoals.


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

3 files changed, 32 insertions, 26 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index f4985f40e1..d03c527f4f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -880,9 +880,10 @@ let add_hint_lemmas eapply lems hint_db gl =
 
 let make_local_hint_db eapply lems gl =
   let sign = pf_hyps gl in
+  let ts = Hint_db.transparent_state (searchtable_map "core") 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 (Hint_db.empty ts 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/class_tactics.ml4 b/tactics/class_tactics.ml4
index 5553f60350..3551b75e52 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -307,24 +307,24 @@ let hints_tac hints =
     in
     let tacs = List.sort compare tacs in
     let rec aux i = function
-      | (_, pp, b, {it = gls; sigma = s}) :: tl ->
+      | (_, pp, b, {it = gls; sigma = s'}) :: tl ->
 	  if !typeclasses_debug then msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
 					       ++ str" on" ++ spc () ++ pr_ev s gl);
 	  let fk =
 	    (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *)
 	    aux (succ i) tl)
 	  in
-	  let sgls = 
+	  let sgls =
 	    evars_to_goals (fun evm ev evi ->
-	    if Typeclasses.is_resolvable evi &&
-	      (not info.only_classes || Typeclasses.is_class_evar evm evi) then
-	      Typeclasses.mark_unresolvable evi, true
-	    else evi, false) s
+			      if Typeclasses.is_resolvable evi &&
+				(not info.only_classes || Typeclasses.is_class_evar evm evi)
+			      then Typeclasses.mark_unresolvable evi, true
+			      else evi, false) s'
 	  in
 	  let newgls, s' =
 	    let gls' = List.map (fun g -> (None, g)) gls in
 	    match sgls with
-	    | None -> gls', s
+	    | None -> gls', s'
 	    | Some (evgls, s') ->
 		(gls' @ List.map (fun (ev, x) -> (Some ev, x)) evgls, s')
 	  in
@@ -333,7 +333,7 @@ let hints_tac hints =
 	      { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
 		is_evar = evar;
 		hints = 
-		  if b && Goal.V82.hyps s g <> Goal.V82.hyps s gl
+		  if b && Goal.V82.hyps s' g <> Goal.V82.hyps s' gl
 		  then make_autogoal_hints info.only_classes
 		    ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'}
 		  else info.hints }
@@ -443,19 +443,6 @@ let resolve_all_evars_once debug (mode, depth) p evd =
   let db = searchtable_map typeclasses_db in
     real_eauto (Hint_db.transparent_state db) [db] p evd
 
-let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
-  let (gl,t,sigma) = 
-    Goal.V82.mk_goal sigma (Environ.named_context_val env) 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 evd = sig_sig gls' 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)
-
 (** We compute dependencies via a union-find algorithm.
     Beware of the imperative effects on the partition structure,
     it should not be shared, but only used locally. *)
@@ -476,6 +463,19 @@ let evar_dependencies evm p =
       in Intpart.union_set evars p)
     evm ()
 
+let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
+  let (gl,t,sigma) = 
+    Goal.V82.mk_goal sigma (Environ.named_context_val env) 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 evd = sig_sig gls' 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)
+
 (** [split_evars] returns groups of undefined evars according to dependencies *)
 
 let split_evars evm =
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 127a61db5e..737b557507 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1029,7 +1029,9 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl =
 	| Some id -> pf_get_hyp_typ gl id, Some id
 	| None -> pf_concl gl, None
       in
-      let res = cl_rewrite_clause_aux ?abs strat (pf_env gl) [] (project gl) concl is_hyp in
+      let sigma = project gl in
+      let concl = Evarutil.nf_evar sigma concl in 
+      let res = cl_rewrite_clause_aux ?abs strat (pf_env gl) [] sigma concl is_hyp in
 	treat res
     with
     | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
@@ -1683,7 +1685,10 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
 
 let get_hyp gl evars (c,l) clause l2r =
   let hi = decompose_applied_relation (pf_env gl) evars None (c,l) l2r in
-  let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
+  let but = match clause with
+    | Some id -> pf_get_hyp_typ gl id 
+    | None -> Evarutil.nf_evar evars (pf_concl gl)
+  in
     unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl
 
 let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
@@ -1702,8 +1707,8 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
     try
       tclWEAK_PROGRESS 
 	(tclTHEN
-            (Refiner.tclEVARS hypinfo.cl.evd)
-            (cl_rewrite_clause_tac ~abs:hypinfo.abs strat (mkMeta meta) cl)) gl
+           (Refiner.tclEVARS hypinfo.cl.evd)
+	   (cl_rewrite_clause_tac ~abs:hypinfo.abs strat (mkMeta meta) cl)) gl
     with RewriteFailure ->
       let {l2r=l2r; c1=x; c2=y} = hypinfo in
 	raise (Pretype_errors.PretypeError