diff options
| author | herbelin | 2004-12-25 12:19:39 +0000 |
|---|---|---|
| committer | herbelin | 2004-12-25 12:19:39 +0000 |
| commit | e76a0434a8d88fb49543cedc9b342d8a1f7019b5 (patch) | |
| tree | 74165145f4f45ce38152bc622cec6f0853887227 /parsing/ppconstr.ml | |
| parent | ca0c3c0fe1b032113dbbe4b69b683c5669d79f4b (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@6505 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 4e1f01c62d..c76de59f14 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -222,7 +222,7 @@ let rec pr_cases_pattern _inh = function | CPatNotation (_,"( _ )",[p]) -> str"("++ pr_cases_pattern _inh p ++ str")" | CPatNotation (_,s,env) -> fst (pr_patnotation pr_cases_pattern s env) - | CPatNumeral (_,n) -> Bignat.pr_bigint n + | CPatNumeral (_,n) -> Bigint.pr_bigint n | CPatDelimiters (_,key,p) -> pr_delimiters key (pr_cases_pattern _inh p) let pr_cases_pattern = pr_cases_pattern (0,E) (* level unused *) @@ -320,7 +320,7 @@ let rec pr inherited a = | CNotation (_,"( _ )",[t]) -> str"("++ pr (max_int,E) t ++ str")", latom | CNotation (_,s,env) -> pr_notation pr s env - | CNumeral (_,p) -> Bignat.pr_bigint p, latom + | CNumeral (_,p) -> Bigint.pr_bigint p, latom | CDelimiters (_,sc,a) -> pr_delimiters sc (pr ltop a), latom | CDynamic _ -> str "<dynamic>", latom in |