From e5b3bd6b12af9f08d7913e25748fba9c4f9fd48f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 29 Sep 2018 18:20:36 +0200
Subject: [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`.
---
 pretyping/typeclasses.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping/typeclasses.mli')

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. *)
-- 
cgit v1.2.3