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`.
---
 vernac/lemmas.ml      | 8 ++++++++
 vernac/lemmas.mli     | 6 +++++-
 vernac/obligations.ml | 4 ++--
 3 files changed, 15 insertions(+), 3 deletions(-)

(limited to 'vernac')

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