From a6014aeeb9a515d6120f22ae0bbed029b474b71f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 May 2003 22:38:09 +0000
Subject: Ajout V8Notation

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

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 08ec0d87aa..baedbf4fc7 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -468,9 +468,9 @@ let rec pr_vernac = function
         ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with
     | None -> mt()
     | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
-  | VernacNotation (local,s,c,l,mv8,opt) ->
+  | VernacNotation (local,c,sl,mv8,opt) ->
       let (s,l) = match mv8 with
-          None -> (s,l)
+          None -> out_some sl
         | Some ml -> ml in
       let ps =
 	let n = String.length s in
@@ -486,9 +486,9 @@ let rec pr_vernac = function
       (match opt with
         | None -> mt()
         | Some sc -> str" :" ++ spc() ++ str sc))
-  | VernacSyntaxExtension (local,s,l,mv8) ->
+  | VernacSyntaxExtension (local,sl,mv8) ->
       let (s,l) = match mv8 with
-          None -> (s,l)
+          None -> out_some sl
         | Some ml -> ml in
       str"Uninterpreted Notation" ++ spc() ++ pr_locality local ++ qs s ++
       (match l with | [] -> mt() | _ as l -> 
-- 
cgit v1.2.3