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

5 files changed, 30 insertions, 30 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 9126af23dc..b2489eac19 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -133,8 +133,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
     let c = Command.generalize_constr_expr tclass ctx in
     let c', imps = interp_type_evars_impls ~evdref:isevars env c in
     let ctx, c = Sign.decompose_prod_assum c' in
-    let cl, args = Typeclasses.dest_class_app c in
-      cl, ctx, imps, (List.rev (Array.to_list args))
+    let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in
+      cl, ctx, imps, (List.rev args)
   in
   let id = 
     match snd instid with
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
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index bf9ee12695..c7ba7fa44a 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -382,8 +382,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
     let c = Command.generalize_constr_expr tclass ctx in
     let imps, c' = interp_type_evars isevars env c in
     let ctx, c = decompose_prod_assum c' in
-    let cl, args = Typeclasses.dest_class_app c in
-      cl, ctx, imps, List.rev (Array.to_list args)
+    let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in
+      cl, ctx, imps, List.rev args
   in
   let id = 
     match snd instid with
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ea2d53ff2b..d6ce01bbc6 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -361,16 +361,16 @@ let pr_ne_context_of header footer env =
 
 let explain_typeclass_resolution env evi k =
   match k with
-      InternalHole | ImplicitArg _ ->
-	(match Typeclasses.class_of_constr evi.evar_concl with
-	  | Some c -> 
-	      let env = Evd.evar_env evi in
-		fnl () ++ str "Could not find an instance for " ++ 
-		  pr_lconstr_env env evi.evar_concl ++ 
-		  pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
-	  | None -> mt())
-    | _ -> mt()
-
+  | InternalHole | ImplicitArg _ ->
+      (match Typeclasses.class_of_constr evi.evar_concl with
+      | Some c -> 
+	  let env = Evd.evar_env evi in
+	    fnl () ++ str "Could not find an instance for " ++ 
+	      pr_lconstr_env env evi.evar_concl ++ 
+	      pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
+      | None -> mt())
+  | _ -> mt()
+      
 let explain_unsolvable_implicit env evi k explain =
   str "Cannot infer " ++ explain_hole_kind env k ++ 
   explain_unsolvability explain ++ str "." ++