diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 07f4354b52..d888d6ffac 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -295,14 +295,14 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro | None -> [||], None, termtype in let hook = Lemmas.mk_hook hook in - let ctx = Evd.universe_context_set evm in + let ctx = Evd.evar_universe_context evm in ignore (Obligations.add_definition id ?term:constr typ ctx ~kind:(Global,poly,Instance) ~hook obls); id else (Flags.silently (fun () -> - Lemmas.start_proof id kind (termtype, Evd.universe_context_set evm) + Lemmas.start_proof id kind (Evd.evar_universe_context evm) termtype (Lemmas.mk_hook (fun _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) |