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/declareDef.ml | |
| parent | 13ddbed6afa8a1917e3906c8b92f5bf56d3f2377 (diff) | |
| parent | c8883873426c92778a1cac02da17e3d123beb394 (diff) | |
Merge PR #8704: [vernac] Remove unused abstraction from declaration_hook type.
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 77177dfa41..7426c128cc 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -58,9 +58,9 @@ let declare_definition ident (local, p, k) ce pl imps hook = gr | Discharge | Local | Global -> declare_global_definition ident ce local k pl imps in - Lemmas.call_hook fix_exn hook local r + Lemmas.call_hook fix_exn hook local r; r 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 _ r -> r)) + declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ _ -> ())) |