diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 14 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 3 |
2 files changed, 1 insertions, 16 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 55d9838bbb..67c5643459 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -11,7 +11,6 @@ (*i*) open Names open Globnames -open Decl_kinds open Term open Constr open Vars @@ -482,19 +481,6 @@ let instances r = let is_class gr = GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes -let is_instance = function - | ConstRef c -> - (match Decls.constant_kind c with - | IsDefinition Instance -> true - | _ -> false) - | VarRef v -> - (match Decls.variable_kind v with - | IsDefinition Instance -> true - | _ -> false) - | ConstructRef (ind,_) -> - is_class (IndRef ind) - | _ -> false - (* To embed a boolean for resolvability status. This is essentially a hack to mark which evars correspond to goals and do not need to be resolved when we have nested [resolve_all_evars] diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 80c6d82397..f0437be4ed 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -79,13 +79,12 @@ val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass (** Just return None if not a class *) val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option - + val instance_impl : instance -> GlobRef.t val hint_priority : instance -> int option val is_class : GlobRef.t -> bool -val is_instance : GlobRef.t -> bool (** Returns the term and type for the given instance of the parameters and fields of the type class. *) |