diff options
| author | Emilio Jesus Gallego Arias | 2018-10-11 00:20:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-30 23:14:55 +0100 |
| commit | 3429abee7c572676fa1155bf1620386bdf10d798 (patch) | |
| tree | b85975f0e1e9115ab65902463af9aff356b15c72 /vernac/comDefinition.ml | |
| parent | acd0c18829a03159c489d908ce8f5f510de2f347 (diff) | |
[vernac] [hooks] Refactor towards optional hooks.
We make `declaration_hook`s optional arguments everywhere, and thus we
avoid some "fake" functions having to be passed.
This identifies positively the code really using hooks [funind,
rewrite, coercions, program, and canonicals] and helps moving toward
some hope of reification.
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) |