diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-04 11:53:19 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-04 11:53:19 +0000 |
| commit | 41abdd815f9384e197cba73ee67f2b78f89a6319 (patch) | |
| tree | 9b0d2b502e98e705529d1b244d0eaf8026f72f86 /grammar | |
| parent | 5b6582f8d47975f6f4f394cf44a1c65c799d43ff (diff) | |
Adding a nominal typing layer to Metasyntax in order to clarify
things up. Records are used instead of their equivalents as tuples.
This is maybe syntactically heavier, but this is semantically
equivalent and easier to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15848 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index ce97ee78e..f11927e77 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -124,7 +124,9 @@ 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< ($se$, $make_tags loc pt$, ($level$, $prods$)) >> + <:expr< { Pptactic.pptac_key = $se$; + pptac_args = $make_tags loc pt$; + pptac_prods = ($level$, $prods$) } >> let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) |