diff options
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 d73e80f749..3acf6904b2 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 1d7b8345f3..9963bad73a 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 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 |