diff options
| author | Emilio Jesus Gallego Arias | 2020-06-09 04:18:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:11 +0200 |
| commit | 22bb101bae56a56a7bcdad2562daf5150ee9408b (patch) | |
| tree | 1a3411cab25120a78255aaf9045ce1577a315149 | |
| parent | ba8db3c1a6e40816db12ff986437788aa71abd33 (diff) | |
[declare] Nit on hook call.
| -rw-r--r-- | vernac/declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index fc52c05793..011e00eb2d 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1072,7 +1072,7 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry = in let () = Impargs.maybe_declare_manual_implicits false dref impargs in let () = definition_message name in - Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook; + Hook.call ?hook { Hook.S.uctx; obls; scope; dref }; dref let declare_entry = declare_entry_core ~obls:[] |