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

1 files changed, 11 insertions, 10 deletions

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