Remove some unused values and types

2 files changed, 0 insertions, 85 deletions

diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index b1ff59e78..41f2edfcf 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -153,7 +153,6 @@ module Make (P:Polynom.S) = struct
   type coef = P.t
   let coef0 = P.of_num (Num.Int 0)
   let coef1 = P.of_num (Num.Int 1)
-  let coefm1 = P.of_num (Num.Int (-1))
   let string_of_coef c = "["^(P.to_string c)^"]"
 
 (***********************************************************************
@@ -252,59 +251,6 @@ let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef
   in 
   (stringP p true)
 
-
-
-let print_pol zeroP hdP tlP coefterm monterm string_of_coef
-    dimmon string_of_exp lvar p =
-
-  let rec print_mon m coefone =
-    let s=ref [] in
-    for i=1 to (dimmon m) do
-      (match (string_of_exp m i) with
-        "0" -> ()
-      | "1" -> s:= (!s) @ [(getvar lvar (i-1))]
-      | e -> s:= (!s) @ [((getvar lvar (i-1)) ^ "^" ^ e)]);
-    done;
-    (match !s with
-      [] -> if coefone 
-      then print_string "1"
-      else ()
-    | l -> if coefone 
-    then print_string (String.concat "*" l)
-    else (print_string "*"; 
-          print_string (String.concat "*" l)))
-  and print_term t start = let a = coefterm t and m = monterm t in
-  match (string_of_coef a) with
-    "0" -> ()
-  | "1" ->(match start with
-      true -> print_mon m true
-    |false -> (print_string "+ ";
-               print_mon m true))
-  | "-1" ->(print_string "-";print_space();print_mon m true)
-  | c -> if (String.get c 0)='-'
-  then (print_string "- ";
-        print_string (String.sub c 1 
-                        ((String.length c)-1));
-        print_mon m false)
-  else (match start with
-    true -> (print_string c;print_mon m false)
-  |false -> (print_string "+ ";
-             print_string c;print_mon m false))
-  and printP p start = 
-    if (zeroP p)
-    then (if start 
-    then print_string("0")
-    else ())
-    else (print_term (hdP p) start;
-          if start then open_hovbox 0;
-          print_space();
-          print_cut();
-          printP (tlP p) false)
-  in open_hovbox 3;
-  printP p true;
-  print_flush()
-
-
 let stringP metadata (p : poly) =
   string_of_pol 
     (fun p -> match p with [] -> true | _ -> false)
@@ -595,9 +541,6 @@ let addS x l =    l @ [x] (* oblige de mettre en queue sinon le certificat decon
  critical pairs/s-polynomials
  *)
 
-let ordcpair ((i1,j1),m1) ((i2,j2),m2) =
-  compare_mon m1 m2 
-
 module CPair =
 struct
 type t = (int * int) * Monomial.t
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
  *)