diff options
| author | Pierre-Marie Pédrot | 2018-12-05 17:41:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-05 17:41:33 +0100 |
| commit | ce4910fe9299bbd54a313980eedaf8d57daade1c (patch) | |
| tree | 4b758b6af09181d86f5b614141d4460f34d923e8 /vernac/classes.ml | |
| parent | 23f2222bb2c97110b6e55835fd19528177e41ff3 (diff) | |
| parent | 3429abee7c572676fa1155bf1620386bdf10d798 (diff) | |
Merge PR #8705: [vernac] [hooks] Refactor towards optional hooks.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 7d6bd1ca64..d0cf1c6bee 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -163,10 +163,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 hook = Obligations.mk_univ_hook hook in + let univ_hook = Obligations.mk_univ_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) ~hook obls) + ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~univ_hook obls) else Flags.silently (fun () -> (* spiwack: it is hard to reorder the actions to do @@ -176,7 +176,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) - (Lemmas.mk_hook + ~hook:(Lemmas.mk_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 @@ -423,8 +423,7 @@ let context poly l = | Some b -> let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in - let hook = Lemmas.mk_hook (fun _ _ -> ()) in - let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in + let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus |