diff options
| -rw-r--r-- | library/decls.ml | 3 | ||||
| -rw-r--r-- | library/decls.mli | 6 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 3 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 2 | ||||
| -rw-r--r-- | toplevel/lemmas.ml | 3 |
5 files changed, 10 insertions, 7 deletions
diff --git a/library/decls.ml b/library/decls.ml index be68ce8de..74a5f7ef1 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -55,7 +55,8 @@ let constant_kind kn = Cmap.find kn !csttab (** Miscellaneous functions. *) -let clear_proofs sign = +let initialize_named_context_for_proof () = + let sign = Global.named_context () in List.fold_right (fun (id,c,t as d) signv -> let d = if variable_opacity id then (id,None,t) else d in diff --git a/library/decls.mli b/library/decls.mli index 6de8bd4e6..73f1745b5 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -33,7 +33,11 @@ val variable_exists : variable -> bool val add_constant_kind : constant -> logical_kind -> unit val constant_kind : constant -> 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 : dir_path -> identifier list -val clear_proofs : named_context -> Environ.named_context_val diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 8ff28293b..8021d742b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -955,8 +955,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ try (add_suffix current_proof_name "_subproof") with _ -> anomaly "open_new_goal with an unamed theorem" in - let sign = Global.named_context () in - let sign = clear_proofs sign in + let sign = initialize_named_context_for_proof () in let na = next_global_ident_away name [] in if Termops.occur_existential gls_type then Util.error "\"abstract\" cannot handle existentials"; diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 2c85a26fe..e67c595bd 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -167,7 +167,7 @@ let build_constant_by_tactic id sign typ tac = let build_by_tactic env typ tac = let id = id_of_string ("temporary_proof"^string_of_int (next())) in - let sign = Decls.clear_proofs (named_context env) in + let sign = val_of_named_context (named_context env) in (build_constant_by_tactic id sign typ tac).const_entry_body (**********************************************************************) diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 7f3edefbb..5817ef1b9 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -252,8 +252,7 @@ let start_hook = ref ignore let set_start_hook = (:=) start_hook let start_proof id kind c ?init_tac ?(compute_guard=[]) hook = - let sign = Global.named_context () in - let sign = clear_proofs sign in + let sign = initialize_named_context_for_proof () in !start_hook c; Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook |