diff options
| author | barras | 2003-11-18 18:54:38 +0000 |
|---|---|---|
| committer | barras | 2003-11-18 18:54:38 +0000 |
| commit | b04df941937814d3701c9d0f573d962d85f088cc (patch) | |
| tree | ea67fac2c2aa73271ca47393e49d2ff0d1ee10cf /translate | |
| parent | 9a33fa8f17adab845424b711e8099e743cf140f8 (diff) | |
reparation bug moins unaire (erreur de PP)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4944 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 2b37b945b3..af8fb845de 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -131,6 +131,8 @@ let rec pr_patt inh p = prlist_with_sep sep (pr_patt (lapp,L)) args, lapp | CPatAtom (_,None) -> str "_", latom | CPatAtom (_,Some r) -> pr_reference r, latom + | CPatNotation (_,"( _ )",[p]) -> + str"("++ pr_patt (max_int,E) p ++ str")", latom | CPatNotation (_,s,env) -> pr_notation pr_patt s env | CPatNumeral (_,i) -> Bignat.pr_bigint i, latom | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt lsimple p), 1 @@ -512,6 +514,8 @@ let rec pr inherited a = | CSort (_,s) -> pr_sort s, latom | CCast (_,a,b) -> hv 0 (pr (lcast,L) a ++ cut () ++ str ":" ++ pr (-lcast,E) b), lcast + | CNotation (_,"( _ )",[t]) -> + str"("++ pr (max_int,L) t ++ str")", latom | CNotation (_,s,env) -> pr_notation pr s env | CNumeral (_,(Bignat.POS _ as p)) -> Bignat.pr_bigint p, lposint | CNumeral (_,(Bignat.NEG _ as p)) -> Bignat.pr_bigint p, lnegint |