Merge PR #8596: [api] Cleanup `Decls`: remove unused function, move vernac helper.

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) ->