diff options
| author | Emilio Jesus Gallego Arias | 2019-02-12 22:37:33 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-23 16:53:53 +0100 |
| commit | d31056ec924ef6e09b28bc3822b427b67a8a300b (patch) | |
| tree | d720333732d9be1a03f74cc079e0a1903d31e023 /vernac/classes.ml | |
| parent | c37e90b67c74b32837409a9a424757246067ef1b (diff) | |
[vernac] Unify declaration hooks.
Supersedes #8718.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 39c086eff5..263ebf5f5a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -161,10 +161,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id in obls, Some constr, typ | None -> [||], None, termtype in - let univ_hook = Obligations.mk_univ_hook hook in + let hook = Lemmas.mk_hook hook in let ctx = Evd.evar_universe_context sigma in ignore (Obligations.add_definition id ?term:constr - ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~univ_hook obls) + ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls) else Flags.silently (fun () -> (* spiwack: it is hard to reorder the actions to do @@ -175,7 +175,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id let sigma = Evd.reset_future_goals sigma in Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) ~hook:(Lemmas.mk_hook - (fun _ -> instance_hook k pri global imps ?hook)); + (fun _ _ _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) if not (Option.is_empty term) then let init_refine = |