3 files changed, 15 insertions, 3 deletions
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) ->