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/declareDef.ml | |
| parent | c37e90b67c74b32837409a9a424757246067ef1b (diff) | |
[vernac] Unify declaration hooks.
Supersedes #8718.
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 361ed1a737..7dcd098183 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) ?hook ce pl imps = +let declare_definition ident (local, p, k) ?hook_data 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,11 +49,17 @@ let declare_definition ident (local, p, k) ?hook ce pl imps = in let () = maybe_declare_manual_implicits false gr imps in let () = definition_message ident in - Lemmas.call_hook ~fix_exn ?hook local gr; gr + begin + match hook_data with + | None -> () + | Some (hook, uctx, extra_defs) -> + Lemmas.call_hook ~fix_exn ~hook uctx extra_defs local gr + end; + gr -let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = +let declare_fix ?(opaque = false) ?hook_data (_,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 + declare_definition f kind ?hook_data ce pl imps let check_definition_evars ~allow_evars sigma = let env = Global.env () in |