aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/nsatz/nsatz.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/nsatz/nsatz.ml')
-rw-r--r--plugins/nsatz/nsatz.ml28
1 files changed, 0 insertions, 28 deletions
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index a5b016611..632b9dac1 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -22,7 +22,6 @@ open Utile
let num_0 = Int 0
and num_1 = Int 1
and num_2 = Int 2
-and num_10 = Int 10
let numdom r =
let r' = Ratio.normalize_ratio (ratio_of_num r) in
@@ -35,7 +34,6 @@ module BigInt = struct
type t = big_int
let of_int = big_int_of_int
let coef0 = of_int 0
- let coef1 = of_int 1
let of_num = Num.big_int_of_num
let to_num = Num.num_of_big_int
let equal = eq_big_int
@@ -49,7 +47,6 @@ module BigInt = struct
let div = div_big_int
let modulo = mod_big_int
let to_string = string_of_big_int
- let to_int x = int_of_big_int x
let hash x =
try (int_of_big_int x)
with Failure _ -> 1
@@ -61,15 +58,6 @@ module BigInt = struct
then a
else if lt a b then pgcd b a else pgcd b (modulo a b)
-
- (* signe du pgcd = signe(a)*signe(b) si non nuls. *)
- let pgcd2 a b =
- if equal a coef0 then b
- else if equal b coef0 then a
- else let c = pgcd (abs a) (abs b) in
- if ((lt coef0 a)&&(lt b coef0))
- ||((lt coef0 b)&&(lt a coef0))
- then opp c else c
end
(*
@@ -146,8 +134,6 @@ let mul = function
| (Const n,q) when eq_num n num_1 -> q
| (p,q) -> Mul(p,q)
-let unconstr = mkRel 1
-
let tpexpr =
lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr")
let ttconst = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEc")
@@ -271,20 +257,6 @@ let set_nvars_term nvars t =
| Pow (t1,n) -> aux t1 nvars
in aux t nvars
-let string_of_term p =
- let rec aux p =
- match p with
- | Zero -> "0"
- | Const r -> string_of_num r
- | Var v -> "x"^v
- | Opp t1 -> "(-"^(aux t1)^")"
- | Add (t1,t2) -> "("^(aux t1)^"+"^(aux t2)^")"
- | Sub (t1,t2) -> "("^(aux t1)^"-"^(aux t2)^")"
- | Mul (t1,t2) -> "("^(aux t1)^"*"^(aux t2)^")"
- | Pow (t1,n) -> (aux t1)^"^"^(string_of_int n)
- in aux p
-
-
(***********************************************************************
Coefficients: recursive polynomials
*)