diff options
| author | herbelin | 2003-05-22 22:38:09 +0000 |
|---|---|---|
| committer | herbelin | 2003-05-22 22:38:09 +0000 |
| commit | a6014aeeb9a515d6120f22ae0bbed029b474b71f (patch) | |
| tree | d55d5e1cc1952f49da4b690cb079a0b0074983a0 | |
| parent | 4a7677505b65816a9dcedca6e5091b2beaa903c5 (diff) | |
Ajout V8Notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4064 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | translate/ppvernacnew.ml | 8 |
1 files 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 -> |