From 66eed5340efdfbd41a775cf679213507bb2ac424 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Apr 2003 16:49:47 +0000
Subject: Prise en compte des syntaxes v8 dans Uninterpreted Notation Suite
 mise en place infrastructure pour déclaration de syntaxe simultanée  à la
 déclaration d'inductifs Table séparée pour les précédences de notations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3983 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 translate/ppvernacnew.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'translate')

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 161232a5fc..49e455cbb1 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -474,9 +474,12 @@ let rec pr_vernac = function
       (match opt with
         | None -> mt()
         | Some sc -> str" :" ++ spc() ++ str sc))
-  | VernacSyntaxExtension (local,a,b) ->
-      str"Uninterpreted Notation" ++ spc() ++ pr_locality local ++ qs a ++
-      (match b with | [] -> mt() | _ as l -> 
+  | VernacSyntaxExtension (local,s,l,mv8) ->
+      let (s,l) = match mv8 with
+          None -> (s,l)
+        | Some ml -> ml in
+      str"Uninterpreted Notation" ++ spc() ++ pr_locality local ++ qs s ++
+      (match l with | [] -> mt() | _ as l -> 
 	str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
 
   (* Gallina *)
-- 
cgit v1.2.3