diff options
| author | Emilio Jesus Gallego Arias | 2018-09-29 18:20:36 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-30 14:25:26 +0200 |
| commit | e5b3bd6b12af9f08d7913e25748fba9c4f9fd48f (patch) | |
| tree | 500c76251fd9973e18bd1840839983d9f36b2d71 /pretyping | |
| parent | 081326a7b2c64e8620777aeae7e2275144b65b4b (diff) | |
[api] Cleanup `Decls`: remove unused function, move vernac helper.
It seems these two functions don't belong there. We can remove one,
and place the other actually next to whether their semantics are
necessary.
Note that indeed the whole `Decls` file seems a bit suspicious, why we
do we register this information in a separate table instead of in the
main ones in `Lib` ?
At the suggestion of Gaëtan Gilbert we also remove unused function
`is_instance`.
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. *) |