diff options
| author | herbelin | 2004-12-24 11:25:18 +0000 |
|---|---|---|
| committer | herbelin | 2004-12-24 11:25:18 +0000 |
| commit | 355671c60fa075b64f64e175bada909a4ce759ac (patch) | |
| tree | e2ade8e51a0e377dac068c43d469951274513f89 /translate | |
| parent | 13517a671562062b32fbe90106098854faa46525 (diff) | |
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèques de grands entiers relatifs munis des 4 opérations de base
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6499 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 83871489ef..9057730eec 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -176,7 +176,7 @@ let rec pr_patt sep inh p = | CPatNotation (_,"( _ )",[p]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env - | CPatNumeral (_,i) -> Bignat.pr_bigint i, latom + | CPatNumeral (_,i) -> Bigint.pr_bigint i, latom | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1 in let loc = cases_pattern_loc p in @@ -601,8 +601,9 @@ let rec pr sep inherited a = | CNotation (_,"( _ )",[t]) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom | CNotation (_,s,env) -> pr_notation (pr mt) s env - | CNumeral (_,(Bignat.POS _ as p)) -> Bignat.pr_bigint p, lposint - | CNumeral (_,(Bignat.NEG _ as p)) -> Bignat.pr_bigint p, lnegint + | CNumeral (_,p) -> + Bigint.pr_bigint p, + (if Bigint.is_pos_or_zero p then lposint else lnegint) | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1 | CDynamic _ -> str "<dynamic>", latom in |