diff options
| author | Arnaud Spiwack | 2014-10-21 20:47:32 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-22 07:31:44 +0200 |
| commit | 81b812c0512fb61342e3f43ebc29bf843a079321 (patch) | |
| tree | 518a3e81749db570b7fc1a65be19f1e586cf3ffe /proofs | |
| parent | 9f0f12e4aa2934283fd3fb3c61f977081cb99a3a (diff) | |
Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.
As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.
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 |