aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/lemmas.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/lemmas.ml')
-rw-r--r--vernac/lemmas.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 77e356eb2..5bf419caf 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -209,7 +209,7 @@ let compute_proof_name locality = function
user_err ?loc (pr_id id ++ str " already exists.");
id, pl
| None ->
- next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
+ next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()), None
let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
let t_i = norm t_i in
@@ -487,7 +487,7 @@ let save_proof ?proof = function
let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
| None ->
- let pftree = Pfedit.get_pftreestate () in
+ let pftree = Proof_global.give_me_the_proof () in
let id, k, typ = Pfedit.current_proof_statement () in
let typ = EConstr.Unsafe.to_constr typ in
let universes = Proof.initial_euctx pftree in
@@ -496,7 +496,7 @@ let save_proof ?proof = function
Proof_global.return_proof ~allow_partial:true () in
let sec_vars =
if not !keep_admitted_vars then None
- else match Pfedit.get_used_variables(), pproofs with
+ else match Proof_global.get_used_variables(), pproofs with
| Some _ as x, _ -> x
| None, (pproof, _) :: _ ->
let env = Global.env () in
@@ -504,7 +504,7 @@ let save_proof ?proof = function
let ids_def = Environ.global_vars_set env pproof in
Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
| _ -> None in
- let names = Pfedit.get_universe_binders () in
+ let names = Proof_global.get_universe_binders () in
let evd = Evd.from_ctx universes in
let binders, ctx = Evd.universe_context ?names evd in
Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
@@ -519,7 +519,7 @@ let save_proof ?proof = function
| Some proof -> proof
in
(* if the proof is given explicitly, nothing has to be deleted *)
- if Option.is_empty proof then Pfedit.delete_current_proof ();
+ if Option.is_empty proof then Proof_global.discard_current ();
Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
(* Miscellaneous *)