From 3eaa54c5e29d4241794578646ac6776c2ec2bbd2 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 14 Sep 2008 10:03:17 +0000 Subject: 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 --- pretyping/typeclasses.mli | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'pretyping/typeclasses.mli') diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index ce0975c69..a9f91dc6f 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 -- cgit v1.2.3