diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-22 17:15:43 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-23 17:42:36 +0200 |
| commit | 1fd8e23da73422b17209e2d69a19dca6789bcaed (patch) | |
| tree | 37c854c17adf96424ec95555b24c5e61033f98c2 /proofs/pfedit.ml | |
| parent | aa63497700bb2e75767c1891a961fc06ba329065 (diff) | |
Change the interface of proof_global to take an evar_map instead of a universe context to start proofs.
It was kind of awkward to work with for non-traditionnal kinds of proofs: if you have an evar_universe_context, you got it from a sigma anyway.
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index d3410ea75..0c4250535 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -27,7 +27,7 @@ let delete_all_proofs = Proof_global.discard_all let start_proof (id : Id.t) str ctx hyps c ?init_tac terminator = let goals = [ (Global.env_of_context hyps , c) ] in - Proof_global.start_proof id str ctx goals terminator; + Proof_global.start_proof (Evd.from_env ~ctx (Global.env ())) id str goals terminator; let env = Global.env () in ignore (Proof_global.with_current_proof (fun _ p -> match init_tac with |