diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-18 00:02:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-18 01:15:43 +0200 |
| commit | 243ffa4b928486122075762da6ce8da707e07daf (patch) | |
| tree | 3870e1b1d3059ba13158a73df7c5f3b300e504ce /toplevel/metasyntax.ml | |
| 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/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 |