diff options
| author | Pierre-Marie Pédrot | 2014-08-18 00:02:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-18 01:15:43 +0200 |
| commit | 243ffa4b928486122075762da6ce8da707e07daf (patch) | |
| tree | 3870e1b1d3059ba13158a73df7c5f3b300e504ce /toplevel | |
| parent | 6dd9e003c289a79b0656e7c6f2cc59935997370c (diff) | |
Moving the TacExtend node from atomic to plain tactics.
Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
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 4e3d460ded..e40e8a73a9 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 fb1e0391b5..00733d5eec 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 |