diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 24 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 8 |
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 |