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

8 files changed, 112 insertions, 112 deletions

diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 4673d5f34..7ad53edb9 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -27,11 +27,17 @@ GEXTEND Gram
     [ [ r = Prim.reference -> CPatAtom (loc,Some r)
       | IDENT "_" -> CPatAtom (loc,None)
       (* Hack to parse syntax "(n)" as a natural number *)
-      | "("; G_constr.test_int_rparen; n = bigint; ")" ->
+      | "("; G_constr.test_int_rparen; n = INT; ")" ->
 	  (* Delimiter "N" moved to "nat" in V7 *)
-          CPatDelimiters (loc,"nat",CPatNumeral (loc,n))
+          CPatDelimiters (loc,"nat",CPatNumeral (loc,Bigint.of_string n))
       | "("; p = compound_pattern; ")" -> p
-      | n = bigint -> CPatNumeral (loc,n)
+      | n = INT -> CPatNumeral (loc,Bigint.of_string n)
+      | "-"; n = INT ->
+          let n = Bigint.of_string n in
+          if n = Bigint.zero then
+            CPatNotation(loc,"( _ )",[CPatNumeral (loc,n)])
+          else
+            CPatNumeral (loc,Bigint.neg n)
       | "'"; G_constr.test_ident_colon; key = IDENT; ":"; c = pattern; "'" -> 
           CPatDelimiters (loc,key,c)
     ] ]
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 6f9a11f45..1a509b1e1 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -206,9 +206,9 @@ GEXTEND Gram
       | "?"; n = Prim.natural -> CPatVar (loc, (false,Pattern.patvar_of_int n))
       | bll = binders; c = constr -> abstract_constr loc c bll
       (* Hack to parse syntax "(n)" as a natural number *)
-      | "("; test_int_rparen; n = bigint; ")" ->
+      | "("; test_int_rparen; n = INT; ")" ->
 	  (* Delimiter "N" moved to "nat" in V7 *)
-          CDelimiters (loc,"nat",CNumeral (loc,n))
+          CDelimiters (loc,"nat",CNumeral (loc,Bigint.of_string n))
       | "("; lc1 = lconstr; ":"; c = constr; (bl,body) = product_tail ->
           let id = coerce_to_name lc1 in
 	  CProdN (loc, ([id], c)::bl, body)
@@ -239,7 +239,9 @@ GEXTEND Gram
 	  CNotation(loc, s, cl)
       | s = sort -> CSort (loc, s)
       | v = global -> CRef v
-      | n = bigint -> CNumeral (loc,n)
+      | (b,n) = bigint -> 
+          if n = Bigint.zero & b then CNotation(loc,"( _ )",[CNumeral (loc,n)])
+          else CNumeral (loc,n)
       | "!"; f = global -> CAppExpl (loc,(None,f),[])
       | "'"; test_ident_colon; key = IDENT; ":"; c = constr; "'" -> 
 	  (* Delimiter "N" implicitly moved to "nat" in V7 *)
@@ -365,4 +367,8 @@ GEXTEND Gram
           ((idl, CHole (fst (List.hd idl)))::bl, c2)
       | ")"; c = constr -> ([], c) ] ]
   ;
+  bigint:
+    [ [ i = INT -> true, Bigint.of_string i
+      | "-"; i = INT -> false, Bigint.neg (Bigint.of_string i) ] ]
+  ;
 END;;
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 60299ae8d..5048b6bd8 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -192,7 +192,8 @@ GEXTEND Gram
       | c=match_constr -> c
       | "("; c = operconstr LEVEL "200"; ")" ->
           (match c with
-              CNumeral(_,Bignat.POS _) -> CNotation(loc,"( _ )",[c])
+              CNumeral(_,z) when Bigint.is_pos_or_zero z ->
+                CNotation(loc,"( _ )",[c])
             | _ -> c) ] ]
   ;
   binder_constr:
@@ -230,7 +231,7 @@ GEXTEND Gram
   atomic_constr:
     [ [ g=global -> CRef g
       | s=sort -> CSort(loc,s)
-      | n=INT -> CNumeral (loc,Bignat.POS (Bignat.of_string n))
+      | n=INT -> CNumeral (loc, Bigint.of_string n)
       | "_" -> CHole loc
       | "?"; id=ident -> CPatVar(loc,(false,id)) ] ]
   ;
@@ -303,9 +304,10 @@ GEXTEND Gram
       | "_" -> CPatAtom (loc,None)
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p with
-              CPatNumeral(_,Bignat.POS _) -> CPatNotation(loc,"( _ )",[p])
+              CPatNumeral(_,z) when Bigint.is_pos_or_zero z ->
+                CPatNotation(loc,"( _ )",[p])
             | _ -> p)
-      | n = INT -> CPatNumeral (loc,Bignat.POS(Bignat.of_string n)) ] ]
+      | n = INT -> CPatNumeral (loc, Bigint.of_string n) ] ]
   ;
   binder_list:
     [ [ idl=LIST1 name; bl=LIST0 binder_let -> 
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index 3daf43202..8fe0536eb 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -109,7 +109,7 @@ let _ =
 (*i*)
 open Rawterm
 open Libnames
-open Bignat
+open Bigint
 open Coqlib
 open Symbols
 open Pp
@@ -122,8 +122,7 @@ open Names
 (* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
 
 let nat_of_int dloc n =
-  match n with
-  | POS n ->
+  if is_pos_or_zero n then begin
       if less_than (of_string "5000") n & Options.is_verbose () then begin
 	warning ("You may experience stack overflow and segmentation fault\
                   \nwhile parsing numbers in nat greater than 5000");
@@ -132,27 +131,27 @@ let nat_of_int dloc n =
       let ref_O = RRef (dloc, glob_O) in
       let ref_S = RRef (dloc, glob_S) in
       let rec mk_nat acc n =
-	if is_nonzero n then 
+	if n <> zero then 
 	  mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n)
 	else 
 	  acc
       in 
       mk_nat ref_O n
-  | NEG n ->
+    end
+  else
       user_err_loc (dloc, "nat_of_int",
         str "Cannot interpret a negative number as a number of type nat")
 
 let pat_nat_of_int dloc n name =
-  match n with
-  | POS n -> 
+  if is_pos_or_zero n then
       let rec mk_nat n name =
-	if is_nonzero n then 
+	if n <> zero then 
 	  PatCstr (dloc,path_of_S,[mk_nat (sub_1 n) Anonymous],name)
 	else 
 	  PatCstr (dloc,path_of_O,[],name)
       in 
       mk_nat n name
-  | NEG n ->
+  else
       user_err_loc (dloc, "pat_nat_of_int",
         str "Unable to interpret a negative number in type nat")
 
@@ -168,7 +167,7 @@ let rec int_of_nat = function
 	  
 let uninterp_nat p =
   try 
-    Some (POS (int_of_nat p))
+    Some (int_of_nat p)
   with
     Non_closed_number -> None
 
@@ -180,7 +179,7 @@ let rec int_of_nat_pattern = function
 	  
 let uninterp_nat_pattern p =
   try 
-    Some (POS (int_of_nat_pattern p))
+    Some (int_of_nat_pattern p)
   with
     Non_closed_number -> None
 
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 6973a551d..10ffbecaf 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -33,7 +33,7 @@ let local_make_binding loc a b =
 let local_append l id = l@[id]
 
 GEXTEND Gram
-  GLOBAL: ident natural integer bigint string preident ast
+  GLOBAL: bigint ident natural integer string preident ast
     astlist qualid reference dirpath identref name base_ident var hyp;
 
  (* Compatibility: Prim.var is a synonym of Prim.ident *)
@@ -66,8 +66,8 @@ GEXTEND Gram
     [ [ i = INT -> local_make_posint i ] ]
   ;
   bigint:
-    [ [ i = INT -> Bignat.POS (Bignat.of_string i)
-      | "-"; i = INT -> Bignat.NEG (Bignat.of_string i) ] ]
+    [ [ i = INT -> Bigint.of_string i
+      | "-"; i = INT -> Bigint.neg (Bigint.of_string i) ] ]
   ;
   integer:
     [ [ i = INT      -> local_make_posint i
diff --git a/parsing/g_primnew.ml4 b/parsing/g_primnew.ml4
index b3863b458..14fb119e4 100644
--- a/parsing/g_primnew.ml4
+++ b/parsing/g_primnew.ml4
@@ -79,6 +79,6 @@ GEXTEND Gram
     ] ]
   ;
   bigint: (* Negative numbers are dealt with specially *)
-    [ [ i = INT -> Bignat.POS (Bignat.of_string i) ] ]
+    [ [ i = INT -> (Bigint.of_string i) ] ]
   ;
 END
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index 72f54721a..949b022c1 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -52,14 +52,12 @@ let get_r_sign_ast loc =
   [| -n |] = - [| n |]           for n >= 0
 *)
 
-let int_decomp n = 
-let div2 k = 
-let x = k mod 2 in
-let y = k - x in (x,y/2) in
-let rec list_ch m =
-if m< 2 then [m]
-else let (x1,x2) = div2 m in x1::(list_ch x2)
-in list_ch n
+open Bigint
+
+let rec int_decomp m = 
+  if equal m zero then [0] else
+  if equal m one then [1] else
+  let (b,r) = euclid m two in (if equal b zero then 0 else 1) :: int_decomp r
 
 let _ = if !Options.v7 then
 let r_of_int n dloc =
@@ -75,7 +73,7 @@ let r_of_int n dloc =
   in mk_r list_ch
 in
 let r_of_string s dloc = 
-  r_of_int (int_of_string s) dloc
+  r_of_int (of_string s) dloc
 in
 let rsyntax_create name =
   let e =
@@ -169,7 +167,7 @@ in ()
 
 open Libnames
 open Rawterm
-open Bignat
+open Bigint
 
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
@@ -200,12 +198,11 @@ let r_of_posint dloc n =
     | a::l' -> if a=1 then RApp (dloc, ref_Rplus, [ref_R1; RApp (dloc, ref_Rmult, [a2; mk_r l'])]) else RApp (dloc, ref_Rmult, [a2; mk_r l'])
   in mk_r list_ch
 
-(* int_of_string o bigint_to_string : temporary hack ... *)
-(* utiliser les bigint de caml ? *)
 let r_of_int2 dloc z =
-  match z with
-  | NEG n -> RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (int_of_string (bigint_to_string (POS n)))]) 
-  | POS n -> r_of_posint dloc (int_of_string (bigint_to_string z))
+  if is_strictly_neg z then
+    RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)])
+  else
+    r_of_posint dloc z
 
 (* V8 *)
 let two = mult_2 one
@@ -214,7 +211,7 @@ let four = mult_2 two
 
 (* Unary representation of strictly positive numbers *)
 let rec small_r dloc n =
-  if is_one n then RRef (dloc, glob_R1)
+  if equal one n then RRef (dloc, glob_R1)
   else RApp(dloc,RRef (dloc,glob_Rplus),
             [RRef (dloc, glob_R1);small_r dloc (sub_1 n)])
 
@@ -227,12 +224,13 @@ let r_of_posint dloc n =
       let (q,r) = div2_with_rest n in
       let b = RApp(dloc,RRef(dloc,glob_Rmult),[r2;r_of_pos q]) in
       if r then RApp(dloc,RRef(dloc,glob_Rplus),[r1;b]) else b in
-  if is_nonzero n then r_of_pos n else RRef(dloc,glob_R0)
+  if n <> zero then r_of_pos n else RRef(dloc,glob_R0)
 
 let r_of_int dloc z =
-  match z with
-  | NEG n -> RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc n]) 
-  | POS n -> r_of_posint dloc n
+  if is_strictly_neg z then
+    RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)]) 
+  else
+    r_of_posint dloc z
 
 (**********************************************************************)
 (* Printing R via scopes                                              *)
@@ -268,8 +266,11 @@ in
 bignat_of_r
 
 let bigint_of_r = function
-  | RApp (_,RRef (_,o), [a]) when o = glob_Ropp -> NEG (bignat_of_r a)
-  | a -> POS (bignat_of_r a)
+  | RApp (_,RRef (_,o), [a]) when o = glob_Ropp ->
+      let n = bignat_of_r a in
+      if n = zero then raise Non_closed_number;
+      neg n
+  | a -> bignat_of_r a
 
 let uninterp_r p =
   try
@@ -294,7 +295,7 @@ let bignat_of_pos p =
   let rec transl = function
     | Node (_,"APPLIST",[p; o; a]) when alpha_eq(p,plus) & alpha_eq(o,one)
         -> add_1(transl a)
-    | a when alpha_eq(a,one) -> Bignat.one
+    | a when alpha_eq(a,one) -> Bigint.one
     | _ -> raise Non_closed_number
   in transl p
 in
@@ -306,12 +307,12 @@ let bignat_option_of_pos p =
 in
 let r_printer_Rplus1 p =
   match bignat_option_of_pos p with
-    | Some n -> Some (str (Bignat.to_string (add_1 n)))
+    | Some n -> Some (str (Bigint.to_string (add_1 n)))
     | None -> None
 in
 let r_printer_Ropp p =
   match bignat_option_of_pos p with
-    | Some n -> Some (str "-" ++ str (Bignat.to_string n))
+    | Some n -> Some (str "-" ++ str (Bigint.to_string n))
     | None -> None
 in
 let r_printer_R1 _ =
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 336b043e9..e6cbda712 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -17,7 +17,7 @@ open Ast
 open Extend
 open Topconstr
 open Libnames
-open Bignat
+open Bigint
 
 (**********************************************************************)
 (* V7 parsing via Grammar *)
@@ -36,7 +36,7 @@ let get_z_sign loc =
 let pos_of_bignat xI xO xH x =
   let rec pos_of x =
     match div2_with_rest x with
-      | (q, true) when is_nonzero q -> mkAppC (xI, [pos_of q])
+      | (q, true) when q <> zero -> mkAppC (xI, [pos_of q])
       | (q, false) -> mkAppC (xO, [pos_of q])
       | (_, true) -> xH
   in 
@@ -44,8 +44,8 @@ let pos_of_bignat xI xO xH x =
     
 let z_of_string pos_or_neg s dloc = 
   let ((xI,xO,xH),(aZERO,aPOS,aNEG)) = get_z_sign dloc in
-  let v = Bignat.of_string s in
-  if is_nonzero v then
+  let v = Bigint.of_string s in
+  if v <> zero then
     if pos_or_neg then
       mkAppC (aPOS, [pos_of_bignat xI xO xH v])
     else 
@@ -103,7 +103,7 @@ let rec bignat_of_pos c1 c2 c3 p =
         mult_2 (bignat_of_pos c1 c2 c3 a)
     | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c2) ->
         add_1 (mult_2 (bignat_of_pos c1 c2 c3 a))
-    | a when alpha_eq(a,c3) -> Bignat.one
+    | a when alpha_eq(a,c3) -> Bigint.one
     | _ -> raise Non_closed_number
 in
 let bignat_option_of_pos xI xO xH p =
@@ -120,9 +120,9 @@ let inside_printer posneg std_pr p =
   match (bignat_option_of_pos xI xO xH p) with
     | Some n -> 
 	if posneg then 
-	  (str (Bignat.to_string n))
+	  (str (Bigint.to_string n))
 	else 
-	  (str "(-" ++ str (Bignat.to_string n) ++ str ")")
+	  (str "(-" ++ str (Bigint.to_string n) ++ str ")")
     | None -> 
 	let pr = if posneg then pr_pos else pr_neg in
 	str "(" ++ pr (std_pr (ope("ZEXPR",[p]))) ++ str ")"
@@ -134,9 +134,9 @@ let outside_printer posneg std_pr p =
   match (bignat_option_of_pos xI xO xH p) with
     | Some n -> 
 	if posneg then 
-	  (str "`" ++ str (Bignat.to_string n) ++ str "`")
+	  (str "`" ++ str (Bigint.to_string n) ++ str "`")
 	else 
-	  (str "`-" ++ str (Bignat.to_string n) ++ str "`")
+	  (str "`-" ++ str (Bigint.to_string n) ++ str "`")
       | None -> 
 	  let pr = if posneg then pr_pos else pr_neg in
 	  str "(" ++ pr (std_pr p) ++ str ")"
@@ -177,34 +177,31 @@ let pos_of_bignat dloc x =
   let rec pos_of x =
     match div2_with_rest x with
       | (q,false) -> RApp (dloc, ref_xO,[pos_of q])
-      | (q,true) when is_nonzero q -> RApp (dloc,ref_xI,[pos_of q])
+      | (q,true) when q <> zero -> RApp (dloc,ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in 
   pos_of x
 
-let interp_positive dloc = function
-  | POS n when is_nonzero n -> pos_of_bignat dloc n
-  | _ ->
-      user_err_loc (dloc, "interp_positive",
-        str "Only strictly positive numbers in type \"positive\"!")
+let error_non_positive dloc = 
+  user_err_loc (dloc, "interp_positive",
+    str "Only strictly positive numbers in type \"positive\"")
+
+let interp_positive dloc n =
+  if is_strictly_pos n then pos_of_bignat dloc n
+  else error_non_positive dloc
 
 let rec pat_pos_of_bignat dloc x name =
   match div2_with_rest x with
     | (q,false) -> 
         PatCstr (dloc,path_of_xO,[pat_pos_of_bignat dloc q Anonymous],name)
-    | (q,true) when is_nonzero q -> 
+    | (q,true) when q <> zero -> 
         PatCstr (dloc,path_of_xI,[pat_pos_of_bignat dloc q Anonymous],name)
     | (q,true) ->
         PatCstr (dloc,path_of_xH,[],name)
 
-let error_non_positive dloc = 
-  user_err_loc (dloc, "interp_positive",
-    str "No non-positive numbers in type \"positive\"!")
-
-let pat_interp_positive dloc = function
-  | NEG n -> error_non_positive dloc
-  | POS n ->
-     if is_nonzero n then pat_pos_of_bignat dloc n else error_non_positive dloc
+let pat_interp_positive dloc n =
+  if is_strictly_pos n then pat_pos_of_bignat dloc n else
+    error_non_positive dloc
 
 (**********************************************************************)
 (* Printing positive via scopes                                       *)
@@ -213,12 +210,12 @@ let pat_interp_positive dloc = function
 let rec bignat_of_pos = function
   | RApp (_, RRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
   | RApp (_, RRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | RRef (_, a) when a = glob_xH -> Bignat.one
+  | RRef (_, a) when a = glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
 
 let uninterp_positive p =
   try 
-    Some (POS (bignat_of_pos p))
+    Some (bignat_of_pos p)
   with Non_closed_number -> 
     None
 
@@ -249,38 +246,35 @@ let glob_N0 = ConstructRef path_of_N0
 let glob_Npos = ConstructRef path_of_Npos
 
 let n_of_posint dloc pos_or_neg n = 
-  if is_nonzero n then
+  if n <> zero then
     RApp(dloc, RRef (dloc,glob_Npos), [pos_of_bignat dloc n])
   else 
     RRef (dloc, glob_N0)
 
+let error_negative dloc =
+  user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\"")
+
 let n_of_int dloc n =
-  match n with
-  | POS n -> n_of_posint dloc true n 
-  | NEG n -> 
-      user_err_loc (dloc, "",
-        str "No negative number in type N")
+  if is_pos_or_zero n then n_of_posint dloc true n
+  else error_negative dloc
 
 let pat_n_of_binnat dloc n name = 
-  if is_nonzero n then
+  if n <> zero then
     PatCstr (dloc, path_of_Npos, [pat_pos_of_bignat dloc n Anonymous], name)
   else 
     PatCstr (dloc, path_of_N0, [], name)
 
 let pat_n_of_int dloc n name =
-  match n with
-  | POS n -> pat_n_of_binnat dloc n name
-  | NEG n ->
-      user_err_loc (dloc, "",
-        str "No negative number in type N")
+  if is_pos_or_zero n then pat_n_of_binnat dloc n name
+  else error_negative dloc
 
 (**********************************************************************)
 (* Printing N via scopes                                              *)
 (**********************************************************************)
 
 let bignat_of_n = function
-  | RApp (_, RRef (_,b),[a]) when b = glob_Npos -> POS (bignat_of_pos a)
-  | RRef (_, a) when a = glob_N0 -> POS (Bignat.zero)
+  | RApp (_, RRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a
+  | RRef (_, a) when a = glob_N0 -> Bigint.zero
   | _ -> raise Non_closed_number
 
 let uninterp_n p =
@@ -312,38 +306,30 @@ let glob_ZERO = ConstructRef path_of_ZERO
 let glob_POS = ConstructRef path_of_POS
 let glob_NEG = ConstructRef path_of_NEG
 
-let z_of_posint dloc pos_or_neg n = 
-  if is_nonzero n then
-    let sgn = if pos_or_neg then glob_POS else glob_NEG in
+let z_of_int dloc n = 
+  if n <> zero then
+    let sgn, n =
+      if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
     RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n])
   else 
     RRef (dloc, glob_ZERO)
 
-let z_of_int dloc z =
-  match z with
-  | POS n -> z_of_posint dloc true n 
-  | NEG n -> z_of_posint dloc false n 
-
-let pat_z_of_posint dloc pos_or_neg n name = 
-  if is_nonzero n then
-    let sgn = if pos_or_neg then path_of_POS else path_of_NEG in
+let pat_z_of_int dloc n name = 
+  if n <> zero then
+    let sgn,n =
+      if is_pos_or_zero n then path_of_POS, n else path_of_NEG, Bigint.neg n in
     PatCstr (dloc, sgn, [pat_pos_of_bignat dloc n Anonymous], name)
   else 
     PatCstr (dloc, path_of_ZERO, [], name)
 
-let pat_z_of_int dloc n name =
-  match n with
-  | POS n -> pat_z_of_posint dloc true n name
-  | NEG n -> pat_z_of_posint dloc false n name
-
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
 
 let bigint_of_z = function
-  | RApp (_, RRef (_,b),[a]) when b = glob_POS -> POS (bignat_of_pos a)
-  | RApp (_, RRef (_,b),[a]) when b = glob_NEG -> NEG (bignat_of_pos a)
-  | RRef (_, a) when a = glob_ZERO -> POS (Bignat.zero)
+  | RApp (_, RRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a
+  | RApp (_, RRef (_,b),[a]) when b = glob_NEG -> bignat_of_pos a
+  | RRef (_, a) when a = glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
 
 let uninterp_z p =
@@ -377,7 +363,7 @@ let bignat_of_pos p =
   let rec transl = function
     | Node (_,"APPLIST",[b; a]) when alpha_eq(b,c1) -> mult_2(transl a)
     | Node (_,"APPLIST",[b; a]) when alpha_eq(b,c2) -> add_1(mult_2(transl a))
-    | a when alpha_eq(a,c3) -> Bignat.one
+    | a when alpha_eq(a,c3) -> Bigint.one
     | _ -> raise Non_closed_number
   in transl p
 in
@@ -391,9 +377,9 @@ let z_printer posneg p =
   match bignat_option_of_pos p with
     | Some n -> 
 	if posneg then 
-	  Some (str (Bignat.to_string n))
+	  Some (str (Bigint.to_string n))
 	else 
-	  Some (str "-" ++ str (Bignat.to_string n))
+	  Some (str "-" ++ str (Bigint.to_string n))
     | None -> None
 in
 let z_printer_ZERO _ =