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

1 files changed, 10 insertions, 14 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