diff options
| author | Hugo Herbelin | 2018-10-15 13:21:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-15 13:21:33 +0200 |
| commit | ecf999c8f8a677508d2856c3c8a7cacfa5da3839 (patch) | |
| tree | 56afb575cdc11708a48f82e033ba1ed2ceb31861 /vernac/comDefinition.ml | |
| parent | 13ddbed6afa8a1917e3906c8b92f5bf56d3f2377 (diff) | |
| parent | c8883873426c92778a1cac02da17e3d123beb394 (diff) | |
Merge PR #8704: [vernac] Remove unused abstraction from declaration_hook type.
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index a8d7946429..5d17662d1a 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -127,10 +127,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 = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in + let hook = Obligations.mk_univ_hook (fun _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in ignore(Obligations.add_definition ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in - ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps - (Lemmas.mk_hook - (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) + ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps hook) |