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 /toplevel/classes.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 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 4d23a4181..e034d0674 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -295,7 +295,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro else (Flags.silently (fun () -> - Lemmas.start_proof id kind (Evd.evar_universe_context evm) termtype + Lemmas.start_proof id kind (Evd.from_env ~ctx:(Evd.evar_universe_context evm) Environ.empty_env) termtype (Lemmas.mk_hook (fun _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) |