Fix bug #1940: uncaught exception when searching for a type class.

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

2 files changed, 16 insertions, 16 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 9bcf8116c1..29655841f5 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -317,20 +317,16 @@ let is_implicit_arg k =
       ImplicitArg (ref, (n, id)) -> true
     | InternalHole -> true
     | _ -> false
-  
-let class_of_constr c = 
-  let extract_cl c =
-    try Some (class_info (global_of_constr c)) with _ -> None
-  in
-    match kind_of_term c with
-	App (c, _) -> extract_cl c
-      | _ -> extract_cl c
-
-let dest_class_app c =
-  let cl c = class_info (global_of_constr c) in
-    match kind_of_term c with
-	App (c, args) -> cl c, args
-      | _ -> cl c, [||]
+
+let global_class_of_constr env c = 
+  try class_info (global_of_constr c)
+  with Not_found -> not_a_class env c
+      
+let dest_class_app env c =
+  let cl, args = decompose_app c in
+    global_class_of_constr env cl, args
+
+let class_of_constr c = try Some (fst (dest_class_app (Global.env ()) c)) with _ -> None
 
 (* To embed a boolean for resolvability status.
    This is essentially a hack to mark which evars correspond to 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index ce0975c69e..a9f91dc6f8 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -52,9 +52,13 @@ val add_instance : instance -> unit
 
 val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
 
-val class_of_constr : constr -> typeclass option
-val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *)
 
+(* These raise a UserError if not a class. *)
+val dest_class_app : env -> constr -> typeclass * constr list
+
+(* Just return None if not a class *)
+val class_of_constr : constr -> typeclass option
+  
 val instance_impl : instance -> constant
 
 val is_class : global_reference -> bool