diff options
| author | Pierre-Marie Pédrot | 2018-10-03 14:48:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-03 14:48:43 +0200 |
| commit | 920cc6ba6ee33bf34cd853f6a9a050ed7594e2ce (patch) | |
| tree | c3874e606bdbac3bf6c3f093587e5dda8dae37ec /pretyping/typeclasses.mli | |
| parent | 016f4a302090bcbb4ad47197dda2c60d6f598f6a (diff) | |
| parent | e5b3bd6b12af9f08d7913e25748fba9c4f9fd48f (diff) | |
Merge PR #8596: [api] Cleanup `Decls`: remove unused function, move vernac helper.
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 3 |
1 files changed, 1 insertions, 2 deletions
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. *) |