Merge PR#582: Fix warnings

1 files changed, 1 insertions, 1 deletions

diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 1dd8da12a8..b14fba9758 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -129,7 +129,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let gl = mlexpr_of_clause clause in
   let level = mlexpr_of_int level in
-  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $level$ $gl$ >> in
+  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ ~{ level = $level$ } $gl$ >> in
   declare_str_items loc
     [ <:str_item< do {
         Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$);