Fixes around typeclasses:

- Correct discharge/classify/rebuild for instances.
  Semantic of Global/Local: local by default in sections, global
  by default in modules.
- Fix the discrimination net's handling of type universes, let 
  the unification do it.
- Correct the typeclass resolution tactic so that when extern tactics
  themselves launch class resolution we don't duplicate work.
  Problem reported by Arthur Chargueraud.


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

3 files changed, 56 insertions, 44 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 539821403..ceaf25be0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -53,7 +53,7 @@ type instance = {
   (* Sections where the instance should be redeclared,
      -1 for discard, 0 for none, mutable to avoid redeclarations
      when multiple rebuild_object happen. *)
-  is_global: int ref;
+  is_global: int;
   is_impl: constant;
 }
 
@@ -63,14 +63,12 @@ let instance_impl is = is.is_impl
 
 let new_instance cl pri glob impl =
   let global =
-    if Lib.sections_are_opened () then
-      if glob then Lib.sections_depth ()
-      else -1
-    else 0
+    if glob then Lib.sections_depth ()
+    else -1
   in
     { is_class = cl.cl_impl;
       is_pri = pri ;
-      is_global = ref global ;
+      is_global = global ;
       is_impl = impl }
 
 (*
@@ -194,15 +192,20 @@ let subst_instance (subst,inst) =
       is_impl = fst (Mod_subst.subst_con subst inst.is_impl) }
 
 let discharge_instance (_,inst) =
-  { inst with
+  if inst.is_global <= 0 then None
+  else Some 
+    { inst with 
+      is_global = pred inst.is_global;
       is_class = Lib.discharge_global inst.is_class;
-      is_impl = Lib.discharge_con inst.is_impl}
-
+      is_impl = Lib.discharge_con inst.is_impl }
+    
 let rebuild_instance inst =
-  match !(inst.is_global) with
-    | -1 | 0 -> inst (* TODO : probably a bug here *)
-    | n -> add_instance_hint inst.is_impl inst.is_pri;
-	inst.is_global := pred n; inst
+  add_instance_hint inst.is_impl inst.is_pri;
+  inst
+
+let classify_instance inst =
+  if inst.is_global = -1 then Dispose
+  else Substitute inst
 
 let (instance_input,instance_output) =
   declare_object
@@ -210,8 +213,8 @@ let (instance_input,instance_output) =
       cache_function = cache_instance;
       load_function = (fun _ -> load_instance);
       open_function = (fun _ -> load_instance);
-      classify_function = (fun x -> Substitute x);
-      discharge_function = (fun a -> Some (discharge_instance a));
+      classify_function = classify_instance;
+      discharge_function = discharge_instance;
       rebuild_function = rebuild_instance;
       subst_function = subst_instance }
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index c6f29de8b..94b2eff38 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -69,11 +69,12 @@ let evars_to_goals p evm =
   let goals, evm' =
     Evd.fold
       (fun ev evi (gls, evm') ->
-	if evi.evar_body = Evar_empty
-	  && Typeclasses.is_resolvable evi
-	  (* 	  && not (is_dependent ev evm) *)
-	  && p evm ev evi then ((ev,evi) :: gls, Evd.add evm' ev (Typeclasses.mark_unresolvable evi)) else
-	  (gls, Evd.add evm' ev evi))
+	if evi.evar_body = Evar_empty then
+	  let evi', goal = p evm ev evi in
+	    if goal then 
+	      ((ev,evi) :: gls, Evd.add evm' ev evi')
+	    else (gls, Evd.add evm' ev evi')
+	else (gls, Evd.add evm' ev evi))
       evm ([], Evd.empty)
   in
     if goals = [] then None
@@ -449,8 +450,7 @@ let _ =
 
 let has_undefined p oevd evd =
   Evd.fold (fun ev evi has -> has ||
-    (evi.evar_body = Evar_empty && p oevd ev evi &&
-	(try Typeclasses.is_resolvable (Evd.find oevd ev) with _ -> true)))
+    (evi.evar_body = Evar_empty && snd (p oevd ev evi)))
     evd false
 
 let rec merge_deps deps = function
@@ -478,25 +478,33 @@ let select_evars evs evm =
     evm Evd.empty
 
 let resolve_all_evars debug m env p oevd do_split fail =
-  let oevm =  oevd in
   let split = if do_split then split_evars oevd else [Intset.empty] in
   let p = if do_split then
-    fun comp evd ev evi -> (Intset.mem ev comp || not (Evd.mem oevm ev)) 
-      && p evd ev evi
-    else fun _ -> p
+    fun comp evd ev evi -> 
+      (try let oevi = Evd.find oevd ev in
+	     if Typeclasses.is_resolvable oevi then
+	       Typeclasses.mark_unresolvable evi, (Intset.mem ev comp &&
+						      p evd ev evi)
+	     else evi, false
+	with Not_found ->
+	  Typeclasses.mark_unresolvable evi, p evd ev evi)
+    else fun _ evd ev evi -> 
+      try let oevi = Evd.find oevd ev in
+	    if Typeclasses.is_resolvable oevi then
+	      Typeclasses.mark_unresolvable evi, p evd ev evi
+	    else evi, false
+      with Not_found ->
+	Typeclasses.mark_unresolvable evi, p evd ev evi
   in
-  let rec aux n p evd =
-    if has_undefined p oevm evd then
-      if n > 0 then
-	let evd' = resolve_all_evars_once debug m p evd in
-	  aux (pred n) p evd'
-      else None
-    else Some evd
+  let rec aux p evd =
+    let evd' = resolve_all_evars_once debug m p evd in
+      if has_undefined p oevd evd' then None
+      else Some evd'
   in
   let rec docomp evd = function
     | [] -> evd
     | comp :: comps ->
-	let res = try aux 1 (p comp) evd with Not_found -> None in
+	let res = try aux (p comp) evd with Not_found -> None in
 	  match res with
 	  | None ->
 	      if fail then
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index a2bc95044..7b6d3ea76 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -29,12 +29,12 @@ struct
     let compare = Pervasives.compare
   end
 
-type term_label = 
-  | GRLabel of global_reference
-  | ProdLabel
-  | LambdaLabel
-  | SortLabel of sorts option
-
+  type term_label = 
+    | GRLabel of global_reference
+    | ProdLabel 
+    | LambdaLabel
+    | SortLabel of sorts option
+	
   module Y =  struct 
      type t = term_label
         let compare x y = 
@@ -97,11 +97,11 @@ let constr_pat_discr_st (idpred,cpred) t =
       Some (GRLabel ref, args)
   | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
   | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l)
-  | PSort s, [] ->
+  | PSort s, [] -> 
       let s' = match s with
 	| RProp c -> Some (Prop c)
-	| RType (Some c) -> Some (Type c)
-	| RType None -> None
+	| RType _ -> None 
+	    (* Don't try to be clever about type levels here *)
       in Some (SortLabel s', [])
   | _ -> None
 
@@ -125,7 +125,8 @@ let constr_val_discr_st (idpred,cpred) t =
     | Var id when not (Idpred.mem id idpred) -> Label(GRLabel (VarRef id),l)
     | Prod (n, d, c) -> Label(ProdLabel, [d; c])
     | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l)
-    | Sort s -> Label(SortLabel (Some s), [])
+    | Sort s when is_small s -> Label(SortLabel (Some s), [])
+    | Sort _ -> Label (SortLabel None, [])
     | Evar _ -> Everything
     | _ -> Nothing