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`.
---
 library/decls.ml | 22 ----------------------
 1 file changed, 22 deletions(-)

(limited to 'library/decls.ml')

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:[]
-- 
cgit v1.2.3