diff options
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index fb1e0391b..00733d5ee 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -140,8 +140,7 @@ let extend_atomic_tactic name entries = let add_atomic (id, args) = match args with | None -> () | Some args -> - let loc = Loc.ghost in - let body = Tacexpr.TacAtom (loc, Tacexpr.TacExtend (loc, name, args)) in + let body = Tacexpr.TacML (Loc.ghost, name, args) in Tacenv.register_atomic_ltac (Names.Id.of_string id) body in List.iter add_atomic entries |