diff options
| author | ppedrot | 2013-11-10 04:02:18 +0000 |
|---|---|---|
| committer | ppedrot | 2013-11-10 04:02:18 +0000 |
| commit | 6544bd19001a18aea49c30e94a09649f2dcc61e4 (patch) | |
| tree | d8abecbdac9cf8671e0a2d8167e6327d47e8ac83 /grammar | |
| parent | 36e41e7581c86214a9f0f97436eb96a75b640834 (diff) | |
Removing the dependency of every level of tactic ATSs on glob_tactic_expr.
Instead of putting the body directly in the AST, we register it in a table.
This time it should work properly. Tactic notation are given kernel names to
ensure the unicity of their contents.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 12de0bcbe8..e56f7a34e5 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -125,9 +125,8 @@ let make_one_printing_rule se (pt,_,e) = let level = mlexpr_of_int 0 in (* only level 0 supported here *) let loc = MLast.loc_of_expr e in let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in - <:expr< { Pptactic.pptac_key = $se$; - pptac_args = $make_tags loc pt$; - pptac_prods = ($level$, $prods$) } >> + <:expr< ($se$, { Pptactic.pptac_args = $make_tags loc pt$; + pptac_prods = ($level$, $prods$) }) >> let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) @@ -203,7 +202,7 @@ let declare_tactic loc s c cl = (Pp.str ("Exception in tactic extend " ^ $se$ ^": ")) (Errors.print e)) ]; Egramml.extend_tactic_grammar $se$ $gl$; - List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >> + List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; } >> ] open Pcaml |