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/declareDef.ml | |
| parent | 23f2222bb2c97110b6e55835fd19528177e41ff3 (diff) | |
| parent | 3429abee7c572676fa1155bf1620386bdf10d798 (diff) | |
Merge PR #8705: [vernac] [hooks] Refactor towards optional hooks.
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 2fe03a8ec5..74b59735a9 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -33,7 +33,7 @@ let get_locality id ~kind = function | Local -> true | Global -> false -let declare_definition ident (local, p, k) ce pl imps hook = +let declare_definition ident (local, p, k) ?hook ce pl imps = let fix_exn = Future.fix_exn_of ce.const_entry_body in let gr = match local with | Discharge when Lib.sections_are_opened () -> @@ -49,8 +49,8 @@ let declare_definition ident (local, p, k) ce pl imps hook = in let () = maybe_declare_manual_implicits false gr imps in let () = definition_message ident in - Lemmas.call_hook fix_exn hook local gr; gr + Lemmas.call_hook ~fix_exn ?hook local gr; gr let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ _ -> ())) + declare_definition f kind ce pl imps |