diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-21 20:47:32 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-22 07:31:44 +0200 |
| commit | 81b812c0512fb61342e3f43ebc29bf843a079321 (patch) | |
| tree | 518a3e81749db570b7fc1a65be19f1e586cf3ffe /proofs/pfedit.ml | |
| 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/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 1b0b2f401..cb826bedc 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 |