[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`.

7 files changed, 16 insertions, 50 deletions

diff --git a/library/decls.ml b/library/decls.ml
index 12c820fb7d..b766b6e2cb 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -11,13 +11,10 @@
 (** This module registers tables for some non-logical informations
      associated declarations *)
 
-open Util
 open Names
 open Decl_kinds
 open Libnames
 
-module NamedDecl = Context.Named.Declaration
-
 (** Datas associated to section variables and local definitions *)
 
 type variable_data =
@@ -47,22 +44,3 @@ let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT"
 let add_constant_kind kn k = csttab := Cmap.add kn k !csttab
 
 let constant_kind kn = Cmap.find kn !csttab
-
-(** Miscellaneous functions. *)
-
-let initialize_named_context_for_proof () =
-  let sign = Global.named_context () in
-  List.fold_right
-    (fun d signv ->
-      let id = NamedDecl.get_id d in
-      let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
-      Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
-
-let last_section_hyps dir =
-  Context.Named.fold_outside
-    (fun d sec_ids ->
-      let id = NamedDecl.get_id d in
-      try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids
-      with Not_found -> sec_ids)
-    (Environ.named_context (Global.env()))
-    ~init:[]
diff --git a/library/decls.mli b/library/decls.mli
index d9fc291518..401884736e 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -34,12 +34,3 @@ val variable_exists : variable -> bool
 
 val add_constant_kind : Constant.t -> logical_kind -> unit
 val constant_kind : Constant.t -> logical_kind
-
-(* Prepare global named context for proof session: remove proofs of
-   opaque section definitions and remove vm-compiled code *)
-
-val initialize_named_context_for_proof : unit -> Environ.named_context_val
-
-(** Miscellaneous functions *)
-
-val last_section_hyps : DirPath.t -> Id.t list
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. *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 880a11becd..aa9bd20bf3 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -344,6 +344,14 @@ let universe_proof_terminator compute_guard hook =
 let standard_proof_terminator compute_guard hook =
   universe_proof_terminator compute_guard (fun _ -> hook)
 
+let initialize_named_context_for_proof () =
+  let sign = Global.named_context () in
+  List.fold_right
+    (fun d signv ->
+      let id = NamedDecl.get_id d in
+      let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
+      Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
+
 let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = match terminator with
   | None -> standard_proof_terminator compute_guard hook
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index c9e4876ee3..38683ed6b2 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -56,6 +56,11 @@ val standard_proof_terminator :
 
 val fresh_name_for_anonymous_theorem : unit -> Id.t
 
+(* Prepare global named context for proof session: remove proofs of
+   opaque section definitions and remove vm-compiled code *)
+
+val initialize_named_context_for_proof : unit -> Environ.named_context_val
+
 (** {6 ... } *)
 
 (** A hook the next three functions pass to cook_proof *)
@@ -63,7 +68,6 @@ val set_save_hook : (Proof.t -> unit) -> unit
 
 val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
 
-
 (** [get_current_context ()] returns the evar context and env of the
    current open proof if any, otherwise returns the empty evar context
    and the current global env *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 3987e53bc7..c4a10b4be6 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1102,7 +1102,7 @@ let show_term n =
 let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
                    ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
     ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
-  let sign = Decls.initialize_named_context_for_proof () in
+  let sign = Lemmas.initialize_named_context_for_proof () in
   let info = Id.print n ++ str " has type-checked" in
   let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
@@ -1122,7 +1122,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
 let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
                            ?(kind=Global,false,Definition) ?(reduce=reduce)
     ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
-  let sign = Decls.initialize_named_context_for_proof () in
+  let sign = Lemmas.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->