diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-25 12:19:39 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-25 12:19:39 +0000 |
| commit | e76a0434a8d88fb49543cedc9b342d8a1f7019b5 (patch) | |
| tree | 74165145f4f45ce38152bc622cec6f0853887227 /parsing | |
| 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')
| -rw-r--r-- | parsing/egrammar.ml | 4 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 4 |
3 files changed, 5 insertions, 5 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index d73e80f74..3acf6904b 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -93,7 +93,7 @@ let make_act (f : loc -> constr_expr action_env -> constr_expr) pil = Gramext.action (fun (v:identifier) -> make ((p,CRef (Ident (dummy_loc,v))) :: env) tl) | Some (p, ETBigint) :: tl -> (* non-terminal *) - Gramext.action (fun (v:Bignat.bigint) -> + Gramext.action (fun (v:Bigint.bigint) -> make ((p,CNumeral (dummy_loc,v)) :: env) tl) | Some (p, ETConstrList _) :: tl -> Gramext.action (fun (v:constr_expr list) -> @@ -119,7 +119,7 @@ let make_act_in_cases_pattern (* For Notations *) Gramext.action (fun (v:identifier) -> make ((p,CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))) :: env) tl) | Some (p, ETBigint) :: tl -> (* non-terminal *) - Gramext.action (fun (v:Bignat.bigint) -> + Gramext.action (fun (v:Bigint.bigint) -> make ((p,CPatNumeral (dummy_loc,v)) :: env) tl) | Some (p, ETConstrList _) :: tl -> Gramext.action (fun (v:cases_pattern_expr list) -> diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 1d7b8345f..9963bad73 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -113,7 +113,7 @@ module Prim : val identref : identifier located Gram.Entry.e val base_ident : identifier Gram.Entry.e val natural : int Gram.Entry.e - val bigint : Bignat.bigint Gram.Entry.e + val bigint : Bigint.bigint Gram.Entry.e val integer : int Gram.Entry.e val string : string Gram.Entry.e val qualid : qualid located Gram.Entry.e diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 4e1f01c62..c76de59f1 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 |