diff options
| author | Maxime Dénès | 2019-02-26 10:19:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-26 10:19:18 +0100 |
| commit | 3459155e1c629a2f932c4d4d917b0f69aa89ccf7 (patch) | |
| tree | 8f1db2c3e2a0d89a412c9c19b6ca458160f4c6c4 /vernac/classes.ml | |
| parent | fc76c77ac6e509c1bccc2823ce2037d21a53276a (diff) | |
| parent | d31056ec924ef6e09b28bc3822b427b67a8a300b (diff) | |
Merge PR #9567: [vernac] Unify declaration hooks.
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: mattam82
Reviewed-by: maximedenes
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 = |