diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 7714cc8108..0f96c2b4af 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -171,6 +171,7 @@ let extend_atomic_tactic name entries = | None -> () | Some args -> let open Tacexpr in + let args = List.map (fun a -> TacGeneric a) args in let entry = { mltac_name = name; mltac_index = i } in let body = TacML (Loc.ghost, entry, args) in Tacenv.register_ltac false false (Names.Id.of_string id) body |