diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 4e3d460de..e40e8a73a 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1196,7 +1196,7 @@ let explain_ltac_call_trace last trace loc = let skip_extensions trace = let rec aux = function | (_,Proof_type.LtacAtomCall - (Tacexpr.TacAlias _ | Tacexpr.TacExtend _) as tac) :: tail -> [tac] + (Tacexpr.TacAlias _) as tac) :: tail -> [tac] | _ :: tail -> aux tail | [] -> [] in List.rev (aux (List.rev trace)) 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 |