diff options
| -rw-r--r-- | grammar/tacextend.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index dc8a47864..5a65fe93a 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -170,7 +170,7 @@ let declare_tactic loc s c cl = match cl with let name = <:expr< Libnames.Ident($dloc$, Names.Id.of_string $name$) >> in declare_str_items loc [ <:str_item< do { - let obj () = Tacenv.register_ltac false false [($name$, false, $body$)] in + let obj () = Tacenv.register_ltac False False [($name$, False, $body$)] in try do { Tacenv.register_ml_tactic $se$ $tac$; Mltop.declare_cache_obj obj __coq_plugin_name; } |