diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 7 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 2 |
2 files changed, 5 insertions, 4 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 1b0b2f401b..cb826bedc4 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -25,9 +25,9 @@ let delete_proof = Proof_global.discard let delete_current_proof = Proof_global.discard_current let delete_all_proofs = Proof_global.discard_all -let start_proof (id : Id.t) str ctx hyps c ?init_tac terminator = +let start_proof (id : Id.t) str sigma hyps c ?init_tac terminator = let goals = [ (Global.env_of_context hyps , c) ] in - Proof_global.start_proof (Evd.from_env ~ctx (Global.env ())) id str goals terminator; + Proof_global.start_proof sigma id str goals terminator; let env = Global.env () in ignore (Proof_global.with_current_proof (fun _ p -> match init_tac with @@ -122,7 +122,8 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = - start_proof id goal_kind ctx sign typ (fun _ -> ()); + let evd = Evd.from_env ~ctx Environ.empty_env in + start_proof id goal_kind evd sign typ (fun _ -> ()); try let status = by tac in let _,(const,univs,_) = cook_proof () in diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index acf809a2b6..d77ab667bc 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -56,7 +56,7 @@ val delete_all_proofs : unit -> unit type lemma_possible_guards = Proof_global.lemma_possible_guards val start_proof : - Id.t -> goal_kind -> Evd.evar_universe_context -> named_context_val -> constr -> + Id.t -> goal_kind -> Evd.evar_map -> named_context_val -> constr -> ?init_tac:unit Proofview.tactic -> Proof_global.proof_terminator -> unit |