From 41abdd815f9384e197cba73ee67f2b78f89a6319 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 4 Oct 2012 11:53:19 +0000
Subject: 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
---
 grammar/tacextend.ml4 | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index ce97ee78e2..f11927e77a 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)
 
-- 
cgit v1.2.3