1 files changed, 15 insertions, 29 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 55d9838bbb..7e5815acd1 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -11,7 +11,6 @@
 (*i*)
 open Names
 open Globnames
-open Decl_kinds
 open Term
 open Constr
 open Vars
@@ -223,26 +222,26 @@ let discharge_class (_,cl) =
                              | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
 			    ctx'
       in
-      List.Smart.map (Option.Smart.map Lib.discharge_global) grs
-      @ newgrs
+      grs @ newgrs
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
-  let cl_impl' = Lib.discharge_global cl.cl_impl in
-  if cl_impl' == cl.cl_impl then cl else
+  try
     let info = abs_context cl in
     let ctx = info.Lib.abstr_ctx in
     let ctx, subst = rel_of_variable_context ctx in
     let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
     let context = discharge_context ctx (subst, usubst) cl.cl_context in
     let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
-    let discharge_proj (x, y, z) = x, y, Option.Smart.map Lib.discharge_con z in
-      { cl_univs = cl_univs';
-        cl_impl = cl_impl';
-	cl_context = context;
-	cl_props = props;
-        cl_projs = List.Smart.map discharge_proj cl.cl_projs;
-	cl_strict = cl.cl_strict;
-	cl_unique = cl.cl_unique
-      }
+    let discharge_proj x = x in
+    { cl_univs = cl_univs';
+      cl_impl = cl.cl_impl;
+      cl_context = context;
+      cl_props = props;
+      cl_projs = List.Smart.map discharge_proj cl.cl_projs;
+      cl_strict = cl.cl_strict;
+      cl_unique = cl.cl_unique
+    }
+  with Not_found -> (* not defined in the current section *)
+    cl
 
 let rebuild_class cl = 
   try 
@@ -366,8 +365,8 @@ let discharge_instance (_, (action, inst)) =
     Some (action,
     { inst with 
       is_global = Some (pred n);
-      is_class = Lib.discharge_global inst.is_class;
-      is_impl = Lib.discharge_global inst.is_impl })
+      is_class = inst.is_class;
+      is_impl = inst.is_impl })
     
 
 let is_local i = (i.is_global == None)
@@ -482,19 +481,6 @@ let instances r =
 let is_class gr = 
   GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
 
-let is_instance = function
-  | ConstRef c ->
-      (match Decls.constant_kind c with
-      | IsDefinition Instance -> true
-      | _ -> false)
-  | VarRef v ->
-      (match Decls.variable_kind v with
-      | IsDefinition Instance -> true
-      | _ -> false)
-  | ConstructRef (ind,_) -> 
-      is_class (IndRef ind)
-  | _ -> false
-
 (* To embed a boolean for resolvability status.
    This is essentially a hack to mark which evars correspond to
    goals and do not need to be resolved when we have nested [resolve_all_evars]