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/comDefinition.ml | |
| parent | 23f2222bb2c97110b6e55835fd19528177e41ff3 (diff) | |
| parent | 3429abee7c572676fa1155bf1620386bdf10d798 (diff) | |
Merge PR #8705: [vernac] [hooks] Refactor towards optional hooks.
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 9c80f1d2f5..79d45880fc 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -90,7 +90,7 @@ let check_definition (ce, evd, _, imps) = check_evars_are_solved env evd; ce -let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = +let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = let (ce, evd, univdecl, imps as def) = interp_definition univdecl bl (pi2 k) red_option c ctypopt in @@ -108,8 +108,8 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = Obligations.eterm_obligations env ident evd 0 c typ in let ctx = Evd.evar_universe_context evd in - let hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in + let univ_hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook ?hook l r) in ignore(Obligations.add_definition - ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls) + ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~univ_hook obls) else let ce = check_definition def in - ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps hook) + ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps ?hook) |