- Make typeclass transparency information directly available

- Fix pretyping to consider remaining unif problems with the
  right transparency information.

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

6 files changed, 32 insertions, 20 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 17a1d3c34b..d2c05b9136 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1303,7 +1303,6 @@ let status_changed lev (pbty,_,t1,t2) =
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
   try
-    assert(Evd.is_undefined evd evk1);
     let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
     let evd = match kind_of_term t2 with
       | Evar (evk2,args2 as ev2) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4536cb5704..4a0fe9cd24 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -683,6 +683,15 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  error_unexpected_type_loc
                     (loc_of_glob_constr c) env !evdref tj.utj_val v
 
+  let resolve_evars env evdref fail_evar resolve_classes =
+    if resolve_classes then
+      evdref := (Typeclasses.resolve_typeclasses ~onlyargs:false
+		 ~split:true ~fail:fail_evar env !evdref);
+    (* Resolve eagerly, potentially making wrong choices *)
+    evdref := (try consider_remaining_unif_problems 
+		 ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
+	       with e -> if fail_evar then raise e else !evdref)
+    
   let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
     let c' = match kind with
       | OfType exptyp ->
@@ -691,13 +700,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env evdref lvar c).utj_val 
     in
-      if resolve_classes then
-	evdref := (Typeclasses.resolve_typeclasses ~onlyargs:false
-		   ~split:true ~fail:fail_evar env !evdref);
-      if fail_evar then
-	(* Resolve eagerly, potentially making wrong choices *)
-	evdref := (try consider_remaining_unif_problems env !evdref
-		   with e -> !evdref);
+      resolve_evars env evdref fail_evar resolve_classes;
       let c = if expand_evar then nf_evar !evdref c' else c' in
 	if fail_evar then check_evars env Evd.empty !evdref c;
 	c
@@ -710,18 +713,15 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let understand_judgment sigma env c =
     let evdref = ref sigma in
     let j = pretype empty_tycon env evdref ([],[]) c in
-    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true
-      ~fail:true env !evdref
-    in
-    let evd = consider_remaining_unif_problems env evd in
-    let j = j_nf_evar evd j in
-    check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
-    j
+      resolve_evars env evdref true true;
+      let j = j_nf_evar !evdref j in
+	check_evars env sigma !evdref (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
+	j
 
   let understand_judgment_tcc evdref env c =
     let j = pretype empty_tycon env evdref ([],[]) c in
-    evdref := Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:false env !evdref;
-    j_nf_evar !evdref j
+      resolve_evars env evdref false true;
+      j_nf_evar !evdref j
 
   (* Raw calls to the unsafe inference machine: boolean says if we must
      fail on unresolved evars; the unsafe_judgment list allows us to
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c8a99a315a..5447c21458 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -37,6 +37,10 @@ let register_set_typeclass_transparency =
   (:=) set_typeclass_transparency_ref
 let set_typeclass_transparency gr local c = !set_typeclass_transparency_ref gr local c
 
+let classes_transparent_state_ref = ref (fun () -> assert false)
+let register_classes_transparent_state = (:=) classes_transparent_state_ref
+let classes_transparent_state () = !classes_transparent_state_ref ()
+
 type rels = constr list
 
 (* This module defines type-classes *)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 77567becec..69a472cb51 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -90,6 +90,9 @@ val resolve_one_typeclass : env -> evar_map -> types -> open_constr
 val register_set_typeclass_transparency : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) -> unit
 val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
 
+val register_classes_transparent_state : (unit -> transparent_state) -> unit
+val classes_transparent_state : unit -> transparent_state
+
 val register_add_instance_hint : (global_reference -> bool (* local? *) -> int option -> unit) -> unit
 val register_remove_instance_hint : (global_reference -> unit) -> unit
 val add_instance_hint : global_reference -> bool -> int option -> unit
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 64c5c5a9e4..f754a926d1 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -320,7 +320,8 @@ let hints_tac hints =
 		       match sgls with
 		       | None -> gls', s'
 		       | Some (evgls, s') ->
-			   (gls' @ List.map (fun (ev, x) -> (Some ev, x)) evgls, s')
+			 (* Reorder with dependent subgoals. *)
+			 (gls' @ List.map (fun (ev, x) -> Some ev, x) evgls, s')
 		   in
 		   let gls' = list_map_i
 		     (fun j (evar, g) ->
@@ -601,7 +602,10 @@ let initial_select_evars onlyargs =
     (fun evd ev evi -> Typeclasses.is_class_evar evd evi)
 
 let resolve_typeclass_evars debug m env evd onlyargs split fail =
- resolve_all_evars debug m env (initial_select_evars onlyargs) evd split fail
+  let evd = Evarconv.consider_remaining_unif_problems
+    ~ts:(Typeclasses.classes_transparent_state ()) env evd 
+  in
+    resolve_all_evars debug m env (initial_select_evars onlyargs) evd split fail
 
 let solve_inst debug depth env evd onlyargs split fail =
   resolve_typeclass_evars debug depth env evd onlyargs split fail
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 200bc516a8..9535e9aaaf 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -41,7 +41,9 @@ let _ =
 	Auto.add_hints local [typeclasses_db]
 	  (Auto.HintsResolveEntry
 	     [pri, false, Some inst, constr_of_global inst])) ());
-  Typeclasses.register_set_typeclass_transparency set_typeclass_transparency
+  Typeclasses.register_set_typeclass_transparency set_typeclass_transparency;
+  Typeclasses.register_classes_transparent_state 
+    (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db))
     
 let declare_class g =
   match global g with