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
---
 printing/pptactic.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index d16035fba0..b790c4ea68 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -28,11 +28,17 @@ let pr_global x = Nametab.pr_global_env Idset.empty x
 
 type grammar_terminals = string option list
 
+type pp_tactic = {
+  pptac_key : string;
+  pptac_args : argument_type list;
+  pptac_prods : int * grammar_terminals;
+}
+
   (* Extensions *)
 let prtac_tab = Hashtbl.create 17
 
-let declare_extra_tactic_pprule (s,tags,prods) =
-  Hashtbl.add prtac_tab (s,tags) prods
+let declare_extra_tactic_pprule pt =
+  Hashtbl.add prtac_tab (pt.pptac_key, pt.pptac_args) (pt.pptac_prods)
 
 let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab (s,tags)
 
-- 
cgit v1.2.3