- 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

4 files changed, 23 insertions, 17 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 17a1d3c34..d2c05b913 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 4536cb570..4a0fe9cd2 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 c8a99a315..5447c2145 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 77567bece..69a472cb5 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