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

2 files changed, 0 insertions, 31 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