diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 19:36:45 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:33:39 +0200 |
| commit | 2826683746569b9d78aa01e319315ab554e1619b (patch) | |
| tree | da0933c7169635d9e35003af4d40b0408e7de96d /grammar | |
| parent | 8a3cd2fe699540f1ae5a56917d0f6b951f81d731 (diff) | |
Fix omitted labels in function calls
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.mlp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 1dd8da12a..b14fba975 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$); |