Imported Upstream version 8.5~beta1+dfsg

7 files changed, 137 insertions, 181 deletions

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index f8929d58..eaf95e94 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -98,7 +98,7 @@ Definition PhiR : list R -> PolZ -> R :=
     (InitialRing.gen_phiZ ring0 ring1 add mul opp)).
 
 Definition PEevalR : list R -> PEZ -> R :=
-   PEeval ring0 add mul sub opp
+   PEeval ring0 ring1 add mul sub opp
     (gen_phiZ ring0 ring1 add mul opp)
          N.to_nat pow.
 
@@ -241,7 +241,9 @@ Fixpoint interpret3 t fv {struct t}: R :=
   | (PEpow t1 t2) =>
        let v1  := interpret3 t1 fv in pow v1 (N.to_nat t2)
   | (PEc t1) => (IZR1 t1)
-  | (PEX n) => List.nth (pred (Pos.to_nat n)) fv 0
+  | PEO => 0
+  | PEI => 1
+  | (PEX _ n) => List.nth (pred (Pos.to_nat n)) fv 0
   end.
 
 
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 4bfcc436..8ff82454 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -16,7 +16,6 @@ a polynomial is a sorted list of (coefficient, monomial)
  *)
 
 open Utile
-open List
 
 exception NotInIdeal
 
@@ -134,7 +133,7 @@ let deg m = m.(0)
 
 let mult_mon m m' =
   let d = nvar m in
-  let m'' = Array.create (d+1) 0 in
+  let m'' = Array.make (d+1) 0 in
   for i=0 to d do
     m''.(i)<- (m.(i)+m'.(i));
   done;
@@ -168,7 +167,7 @@ let compare_mon m m' =
 
 let div_mon m m' =
   let d = nvar m in
-  let m'' = Array.create (d+1) 0 in
+  let m'' = Array.make (d+1) 0 in
   for i=0 to d do
     m''.(i)<- (m.(i)-m'.(i));
   done;
@@ -199,7 +198,7 @@ let set_deg m =
 (* lcm *)
 let ppcm_mon m m' =
   let d = nvar m in
-  let m'' = Array.create (d+1) 0 in
+  let m'' = Array.make (d+1) 0 in
   for i=1 to d do
     m''.(i)<- (max m.(i) m'.(i));
   done;
@@ -215,13 +214,13 @@ let ppcm_mon m m' =
 let repr p = p
 
 let equal =
-  Util.list_for_all2eq
+  Util.List.for_all2eq
     (fun (c1,m1) (c2,m2) -> P.equal c1 c2 && m1=m2)
 
 let hash p =
-  let c = map fst p in
-  let m = map snd p in
-  fold_left (fun h p -> h * 17 + P.hash p) (Hashtbl.hash m) c
+  let c = List.map fst p in
+  let m = List.map snd p in
+  List.fold_left (fun h p -> h * 17 + P.hash p) (Hashtbl.hash m) c
 
 module Hashpol = Hashtbl.Make(
   struct
@@ -236,9 +235,8 @@ module Hashpol = Hashtbl.Make(
 open Format
 
 let getvar lv i =
-  try (nth lv i)
-  with e when Errors.noncritical e ->
-    (fold_left (fun r x -> r^" "^x) "lv= " lv)
+  try (List.nth lv i)
+  with Failure _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv)
     ^" i="^(string_of_int i)
 
 let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef
@@ -363,8 +361,8 @@ let stringPcut p =
   (*Polynomesrec.nsP1:=20;*)
   nsP2:=10;
   let res =
-    if (length p)> !nsP2
-    then (stringP [hd p])^" + "^(string_of_int (length p))^" terms"
+    if (List.length p)> !nsP2
+    then (stringP [List.hd p])^" + "^(string_of_int (List.length p))^" terms"
     else  stringP p in
   (*Polynomesrec.nsP1:= max_int;*)
   nsP2:= max_int;
@@ -399,7 +397,7 @@ let zeroP = []
 
 (* returns a constant polynom ial with d variables *)
 let polconst d c =
-  let m = Array.create (d+1) 0 in
+  let m = Array.make (d+1) 0 in
   let m = set_deg m in 
   [(c,m)]
 
@@ -432,7 +430,7 @@ let coef_of_int x = P.of_num (Num.Int x)
 
 (* variable i *)
 let gen d i =
-  let m = Array.create (d+1) 0 in
+  let m = Array.make (d+1) 0 in
   m.(i) <- 1;
   let m = set_deg m in 
   [((coef_of_int 1),m)]
@@ -463,10 +461,10 @@ let puisP p n=
   match p with
     [] -> []
   |_ ->
-      let d = nvar (snd (hd p)) in
+      let d = nvar (snd (List.hd p)) in
       let rec puisP n =
 	match n with
-	  0 -> [coef1, Array.create (d+1) 0]
+	  0 -> [coef1, Array.make (d+1) 0]
 	| 1 -> p
 	|_ -> multP p (puisP (n-1))
       in puisP n
@@ -484,7 +482,7 @@ let contentPlist lp =
   match lp with
   |[] -> coef1
   |p::l1 ->
-      fold_left
+      List.fold_left
 	(fun r q ->
 	  if P.equal r coef1 || P.equal r coefm1
 	  then r
@@ -501,17 +499,17 @@ let polynom0 =  {pol = ref []; num = 0; sugar = 0}
    
 let ppol p = !(p.pol)
 
-let lm p = snd (hd (ppol p))
+let lm p = snd (List.hd (ppol p))
 
 let nallpol = ref 0
 
-let allpol = ref (Array.create 1000 polynom0)
+let allpol = ref (Array.make 1000 polynom0)
 
 let new_allpol p s =
   nallpol := !nallpol + 1;
   if !nallpol >= Array.length !allpol
   then
-    allpol := Array.append !allpol (Array.create !nallpol polynom0);
+    allpol := Array.append !allpol (Array.make !nallpol polynom0);
   let p = {pol = ref p; num = !nallpol; sugar = s} in
   !allpol.(!nallpol)<- p;
   p
@@ -521,7 +519,7 @@ let new_allpol p s =
 let rec selectdiv m l =
   match l with
     [] -> polynom0
-  |q::r -> let m'= snd (hd (ppol q)) in
+  |q::r -> let m'= snd (List.hd (ppol q)) in
     match (div_mon_test m m') with
       true -> q
     |false -> selectdiv m r
@@ -550,7 +548,7 @@ let div_coef a b = P.divP a b
 (* remainder r of the division of p by polynomials of l, returns (c,r) where c is the coefficient for pseudo-division : c p = sum_i q_i p_i + r *)
 
 let reduce2 p l =
-  let l = if nouveaux_pol_en_tete then rev l else l in
+  let l = if nouveaux_pol_en_tete then List.rev l else l in
   let rec reduce p =
     match p with
       [] -> (coef1,[])
@@ -601,8 +599,8 @@ let coefpoldep_set p q c =
 
 let initcoefpoldep d lp =
   poldep:=lp;
-  poldepcontent:= map (fun p -> contentP (ppol p)) lp;
-  iter
+  poldepcontent:= List.map (fun p -> contentP (ppol p)) lp;
+  List.iter
     (fun p -> coefpoldep_set p p (polconst d (coef_of_int 1)))
     lp
 
@@ -610,7 +608,7 @@ let initcoefpoldep d lp =
    divides without pseudodivisions *)
 
 let reduce2_trace p l lcp =
-  let l = if nouveaux_pol_en_tete then rev l else l in
+  let l = if nouveaux_pol_en_tete then List.rev l else l in
   (* rend (lq,r), ou r = p + sum(lq) *)
   let rec reduce p =
     match p with
@@ -646,10 +644,10 @@ let reduce2_trace p l lcp =
      info ((stringP x)^"\n"))
      lq;
      info "ok\n";*)
-  (map2
+  (List.map2
      (fun c0 q ->
        let c =
-	 fold_left
+	 List.fold_left
 	   (fun x (a,m,s) ->
 	     if equal (ppol s) (ppol q)
 	     then
@@ -672,7 +670,7 @@ let pol_courant = ref polynom0
 let sugar_flag = ref true
 
 let compute_sugar p =
-  fold_left (fun s (a,m) -> max s m.(0)) 0 p
+  List.fold_left (fun s (a,m) -> max s m.(0)) 0 p
 
 let mk_polynom p = 
   new_allpol p (compute_sugar p)
@@ -680,12 +678,12 @@ let mk_polynom p =
 let spol ps qs=
   let p = ppol ps in
   let q = ppol qs in
-  let m = snd (hd p) in
-  let m'= snd (hd q) in
-  let a = fst (hd p) in
-  let b = fst (hd q) in
-  let p'= tl p in
-  let q'= tl q in
+  let m = snd (List.hd p) in
+  let m'= snd (List.hd q) in
+  let a = fst (List.hd p) in
+  let b = fst (List.hd q) in
+  let p'= List.tl p in
+  let q'= List.tl q in
   let c = (pgcdpos a b) in
   let m''=(ppcm_mon m m') in
   let m1 = div_mon m'' m in
@@ -709,8 +707,8 @@ let spol ps qs=
   
 
 let etrangers p p'=
-  let m = snd (hd p) in
-  let m'= snd (hd p') in
+  let m = snd (List.hd p) in
+  let m'= snd (List.hd p') in
   let d = nvar m in
   let res=ref true in
   let i=ref 1 in
@@ -723,9 +721,9 @@ let etrangers p p'=
 (* teste if head monomial of p'' divides lcm of lhead monomials of p and p' *)
 
 let div_ppcm p p' p'' =
-  let m = snd (hd p) in
-  let m'= snd (hd p') in
-  let m''= snd (hd p'') in
+  let m = snd (List.hd p) in
+  let m'= snd (List.hd p') in
+  let m''= snd (List.hd p'') in
   let d = nvar m in
   let res=ref true in
   let i=ref 1 in
@@ -766,7 +764,7 @@ let slice i a q =
 
 (* sugar strategy *)
 
-let rec addS x l =    l @ [x] (* oblige de mettre en queue sinon le certificat deconne *)
+let addS x l =    l @ [x] (* oblige de mettre en queue sinon le certificat deconne *)
 			  
 let addSsugar x l =
   if !sugar_flag
@@ -823,10 +821,10 @@ let ordcpair ((i1,j1),m1) ((i2,j2),m2) =
   compare_mon m1 m2 
 
 let sortcpairs lcp = 
-  sort ordcpair lcp
+  List.sort ordcpair lcp
 
 let mergecpairs l1 l2 =
-  merge ordcpair l1 l2 
+  List.merge ordcpair l1 l2 
 
 let ord i j =
   if i<j then (i,j) else (j,i)
@@ -838,7 +836,7 @@ let cpair p q =
 	 ppcm_mon (lm p) (lm q))]
       
 let cpairs1 p lq =
-  sortcpairs (fold_left (fun r q -> r @ (cpair p q)) [] lq)
+  sortcpairs (List.fold_left (fun r q -> r @ (cpair p q)) [] lq)
     
 let cpairs lp =
   let rec aux l =
@@ -849,18 +847,18 @@ let cpairs lp =
     
     
 let critere2 ((i,j),m) lp lcp =
-  exists
+  List.exists
     (fun h ->
       h.num <> i && h.num <> j
         && (div_mon_test m (lm h))
 	&& (let c1 = ord i h.num in
-	not (exists (fun (c,_) -> c1 = c) lcp))
+	not (List.exists (fun (c,_) -> c1 = c) lcp))
 	&& (let c1 = ord j h.num in
-	not (exists (fun (c,_) -> c1 = c) lcp)))
+	not (List.exists (fun (c,_) -> c1 = c) lcp)))
     lp
 
 let critere3 ((i,j),m) lp lcp =
-  exists
+  List.exists
     (fun h ->
       h.num <> i && h.num <> j
         && (div_mon_test m (lm h))
@@ -881,8 +879,8 @@ let step = ref 0
 
 let infobuch p q =
   if !step = 0 
-  then (info ("[" ^ (string_of_int (length p))
-              ^ "," ^  (string_of_int (length q))
+  then (info ("[" ^ (string_of_int (List.length p))
+              ^ "," ^  (string_of_int (List.length q))
               ^ "]"))
 
 (* in lp new polynomials are at the end *)
@@ -900,13 +898,13 @@ let test_dans_ideal p lp lp0 =
   pol_courant:= mk_polynom r;
   if r=[]
   then (info "polynomial reduced to 0\n";
-	let lcp = map (fun q -> []) !poldep in
+	let lcp = List.map (fun q -> []) !poldep in
 	let c = !coef_courant in
 	let (lcq,r) = reduce2_trace (emultP c p) lp lcp in
 	info "r ok\n";
 	info ("r: "^(stringP r)^"\n");
         let res=ref  (emultP c p) in
-	iter2
+	List.iter2
 	  (fun cq q -> res:=plusP (!res) (multP cq (ppol q));
 	  )
 	  lcq !poldep;
@@ -916,22 +914,22 @@ let test_dans_ideal p lp lp0 =
 	  match lp with
 	  |[] -> []
 	  |p::lp ->
-	      (map
+	      (List.map
 		 (fun q -> coefpoldep_find p q)
 		 lp)::(aux lp)
 	in
 	let coefficient_multiplicateur = c in
-	let liste_polynomes_de_depart = rev lp0 in
+	let liste_polynomes_de_depart = List.rev lp0 in
 	let polynome_a_tester = p in
 	let liste_des_coefficients_intermediaires =
-	  (let lci = rev (aux (rev lp)) in
+	  (let lci = List.rev (aux (List.rev lp)) in
 	  let lci = ref lci (* (map rev lci) *) in
-	  iter (fun x -> lci := tl (!lci)) lp0;
+	  List.iter (fun x -> lci := List.tl (!lci)) lp0;
 	  !lci) in
 	let liste_des_coefficients =
-	  map
+	  List.map
 	    (fun cq -> emultP (coef_of_int (-1)) cq)
-	    (rev lcq) in
+	    (List.rev lcq) in
 	(liste_polynomes_de_depart,
 	 polynome_a_tester,
 	 {coef = coefficient_multiplicateur;
@@ -946,7 +944,7 @@ let test_dans_ideal p lp lp0 =
 let divide_rem_with_critical_pair = ref false
 
 let list_diff l x =
-  filter (fun y -> y <> x) l
+  List.filter (fun y -> y <> x) l
 
 let deg_hom p =
   match p with
@@ -984,12 +982,12 @@ let pbuchf pq p lp0=
 (*		info "pair reduced\n";*)
 		  a.pol := emultP ca (ppol a);
 		  let (lca,a0) = reduce2_trace (ppol a) lp
-		      (map (fun q -> emultP ca (coefpoldep_find a q))
+		      (List.map (fun q -> emultP ca (coefpoldep_find a q))
 			 !poldep) in
 (*		info "paire re-reduced";*)
 		  a.pol := a0;
 (*		  let a0 = new_allpol a0 sa in*)
-		  iter2 (fun c q ->
+		  List.iter2 (fun c q ->
 		    coefpoldep_remove a q;
 		    coefpoldep_set a q c) lca !poldep;
 		  let a0 = a in
@@ -1009,7 +1007,7 @@ let is_homogeneous p =
   match p with
   | [] -> true
   | (a,m)::p1 -> let d = m.(0) in
-    for_all (fun (b,m') -> m'.(0)=d) p1
+    List.for_all (fun (b,m') -> m'.(0)=d) p1
     
 (* returns
    c
@@ -1030,15 +1028,15 @@ let in_ideal d lp p =
   Hashtbl.clear hmon;
   Hashtbl.clear coefpoldep;
   nallpol := 0;
-  allpol := Array.create 1000 polynom0;
-  homogeneous := for_all is_homogeneous (p::lp);
+  allpol := Array.make 1000 polynom0;
+  homogeneous := List.for_all is_homogeneous (p::lp);
   if !homogeneous then info "homogeneous polynomials\n";
   info ("p: "^(stringPcut p)^"\n");
-  info ("lp:\n"^(fold_left (fun r p -> r^(stringPcut p)^"\n") "" lp));
+  info ("lp:\n"^(List.fold_left (fun r p -> r^(stringPcut p)^"\n") "" lp));
   (*info ("p: "^(stringP p)^"\n");
   info ("lp:\n"^(fold_left (fun r p -> r^(stringP p)^"\n") "" lp));*)
 
-  let lp = map mk_polynom lp in
+  let lp = List.map mk_polynom lp in
   let p = mk_polynom p in
   initcoefpoldep d lp;
   coef_courant:=coef1;
@@ -1049,7 +1047,7 @@ let in_ideal d lp p =
     with NotInIdeal -> pbuchf (lp, (cpairs lp)) p lp in
   info "computed\n";
 
-  (map ppol lp1, p1, cert)
+  (List.map ppol lp1, p1, cert)
     
 (* *)
 end
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index a66bd44b..b4eb57ec 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -1,42 +1,24 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Pp
+open Errors
 open Util
-open Names
 open Term
-open Closure
-open Environ
-open Libnames
 open Tactics
-open Glob_term
-open Tacticals
-open Tacexpr
-open Pcoq
-open Tactic
-open Constr
-open Proof_type
 open Coqlib
-open Tacmach
-open Mod_subst
-open Tacinterp
-open Libobject
-open Printer
-open Declare
-open Decl_kinds
-open Entries
 
 open Num
-open Unix
 open Utile
 
+DECLARE PLUGIN "nsatz_plugin"
+
 (***********************************************************************
  Operations on coefficients
 *)
@@ -74,7 +56,7 @@ module BigInt = struct
   let to_int x = int_of_big_int x
   let hash x =
     try (int_of_big_int x)
-    with _-> 1
+    with Failure _ -> 1
   let puis = power_big_int_positive_int
 
   (* a et b positifs, résultat positif *)
@@ -156,7 +138,7 @@ type term =
 
 let const n =
   if eq_num n num_0 then Zero else Const n
-let pow(p,i) = if i=1 then p else Pow(p,i)
+let pow(p,i) = if Int.equal i 1 then p else Pow(p,i)
 let add = function
     (Zero,q) -> q
   | (p,Zero) -> p
@@ -212,7 +194,7 @@ let rec mkt_pos n =
     mkt_app pxI [mkt_pos (quo_num n num_2)]
 
 let mkt_n n =
-  if n=num_0
+  if Num.eq_num n num_0
   then Lazy.force nN0
   else mkt_app nNpos [mkt_pos n]
 
@@ -232,7 +214,7 @@ let rec mkt_term t  =  match t with
 | Add (t1,t2) -> mkt_app  ttadd [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Sub (t1,t2) -> mkt_app  ttsub [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Mul (t1,t2) -> mkt_app  ttmul [Lazy.force tz; mkt_term t1; mkt_term t2]
-| Pow (t1,n) ->  if (n = 0) then
+| Pow (t1,n) ->  if Int.equal n 0 then
     mkt_app ttconst [Lazy.force tz; mkt_z num_1]
 else
     mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)]
@@ -331,7 +313,7 @@ let term_pol_sparse np t=
     match t with
     | Zero -> zeroP
     | Const r ->
-	if r = num_0
+	if Num.eq_num r num_0
 	then zeroP
 	else polconst d (Poly.Pint (Coef.of_num r))
     | Var v ->
@@ -385,19 +367,19 @@ let pol_sparse_to_term n2 p =
 		if m.(k)>0
 		then i0:=k
 	      done;
-	      if !i0 = 0
+	      if Int.equal !i0 0
 	      then (r,d)
 	      else if !i0 > r
 	      then (!i0, m.(!i0))
-	      else if !i0 = r && m.(!i0)<d
+	      else if Int.equal !i0 r && m.(!i0)<d
 	      then (!i0, m.(!i0))
 	      else (r,d))
 	  (0,0)
 	  p in
-      if i0=0
+      if Int.equal i0 0
       then
 	let mp = ref (polrec_to_term a) in
-        if p1=[]
+        if List.is_empty p1
 	then !mp
 	else add(!mp,aux p1)
       else (
@@ -411,7 +393,7 @@ let pol_sparse_to_term n2 p =
 	     else p2:=(a,m)::(!p2))
 	  p;
 	let vm =
-	  if e0=1
+	  if Int.equal e0 1
 	  then Var (string_of_int (i0))
 	  else pow (Var (string_of_int (i0)),e0) in
 	add(mul(vm, aux (List.rev (!p1))), aux (List.rev (!p2))))
@@ -419,13 +401,13 @@ let pol_sparse_to_term n2 p =
   aux p
 
 
-let rec remove_list_tail l i =
+let remove_list_tail l i =
   let rec aux l i =
-    if l=[]
+    if List.is_empty l
     then []
     else if i<0
     then l
-    else if i=0
+    else if Int.equal i 0
     then List.tl l
     else
       match l with
@@ -447,7 +429,7 @@ let rec remove_list_tail l i =
 let remove_zeros zero lci =
   let n = List.length (List.hd lci) in
   let m=List.length lci in
-  let u = Array.create m false in
+  let u = Array.make m false in
   let rec utiles k =
     if k>=m
     then ()
@@ -543,7 +525,7 @@ let theoremedeszeros_termes lp =
 	  let (cert,lp0,p,_lct) = theoremedeszeros lpol p in
           info "cert ok\n";
 	  let lc = cert.last_comb::List.rev cert.gb_comb in
-	  match remove_zeros (fun x -> x=zeroP) lc with
+	  match remove_zeros (fun x -> equal x zeroP) lc with
 	  | [] -> assert false
 	  | (lq::lci) ->
 	      (* lci commence par les nouveaux polynomes *)
@@ -610,7 +592,7 @@ let nsatz_compute t =
   return_term lpol
 
 TACTIC EXTEND nsatz_compute
-| [ "nsatz_compute"  constr(lt) ] -> [ nsatz_compute lt ]
+| [ "nsatz_compute"  constr(lt) ] -> [ Proofview.V82.tactic (nsatz_compute lt) ]
 END
 
 
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index 026b66c7..a9651304 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -1,14 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 (* Recursive polynomials: R[x1]...[xn]. *)
-open Utile
 open Util
+open Utile
 
 (* 1. Coefficients: R *)
 
@@ -133,7 +133,7 @@ let x n = Prec (n,[|cf0;cf1|])
 let monome v n =
   match n with
       0->Pint coef1;
-    |_->let tmp = Array.create (n+1) (Pint coef0) in
+    |_->let tmp = Array.make (n+1) (Pint coef0) in
         tmp.(n)<-(Pint coef1);
         Prec (v, tmp)
 
@@ -159,28 +159,21 @@ let rec max_var_pol2 p =
       Pint _ -> 0
     |Prec(v,c)-> Array.fold_right (fun q m -> max (max_var_pol2 q) m) c v
 
-let rec max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0
+let max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0
 
 (* equality between polynomials *)
 
 let rec equal p q =
   match (p,q) with
       (Pint a,Pint b) -> C.equal a b
-    |(Prec(x,p1),Prec(y,q1)) ->
-       if x<>y then false
-       else if (Array.length p1)<>(Array.length q1) then false
-       else (try (Array.iteri (fun i a -> if not (equal a q1.(i))
-			       then failwith "raté")
-		    p1;
-		  true)
-	     with e when Errors.noncritical e -> false)
+    |(Prec(x,p1),Prec(y,q1)) -> (Int.equal x y) && Array.for_all2 equal p1 q1
     | (_,_) -> false
 
 (* normalize polynomial: remove head zeros, coefficients are normalized
    if constant, returns the coefficient
 *)
 
-let rec norm p = match p with
+let norm p = match p with
     Pint _ -> p
   |Prec (x,a)->
      let d = (Array.length a -1) in
@@ -189,17 +182,17 @@ let rec norm p = match p with
 	 n:=!n-1;
        done;
        if !n<0 then Pint coef0
-       else if !n=0 then a.(0)
-       else if !n=d then p
-       else (let b=Array.create (!n+1) (Pint coef0) in
+       else if Int.equal !n 0 then a.(0)
+       else if Int.equal !n d then p
+       else (let b=Array.make (!n+1) (Pint coef0) in
                for i=0 to !n do b.(i)<-a.(i);done;
                Prec(x,b))
 
 
 (* degree in v, v >= max var of p *)
-let rec deg v p =
+let deg v p =
   match p with
-      Prec(x,p1) when x=v -> Array.length p1 -1
+      Prec(x,p1) when Int.equal x v -> Array.length p1 -1
     |_ -> 0
 
 
@@ -219,8 +212,8 @@ let rec copyP p =
 (* coefficient of degree i in v, v >= max var of p *)
 let coef v i p =
   match p with
-      Prec (x,p1) when x=v  -> if i<(Array.length p1) then p1.(i) else Pint coef0
-    |_ -> if i=0 then p else Pint coef0
+      Prec (x,p1) when Int.equal x v  -> if i<(Array.length p1) then p1.(i) else Pint coef0
+    |_ -> if Int.equal i 0 then p else Pint coef0
 
 (* addition *)
 
@@ -243,7 +236,7 @@ let rec plusP p q =
                               Prec (x,p2))
           else
             (let n=max (deg x p) (deg x q) in
-             let r=Array.create (n+1) (Pint coef0) in
+             let r=Array.make (n+1) (Pint coef0) in
                for i=0 to n do
                  r.(i)<- plusP (coef x i p) (coef x i q);
                done;
@@ -275,15 +268,15 @@ let rec vars=function
 
 
 (* multiply p by v^n, v >= max_var p *)
-let rec multx n v p =
+let multx n v p =
   match p with
-      Prec (x,p1) when x=v -> let p2= Array.create ((Array.length p1)+n) (Pint coef0) in
+      Prec (x,p1) when Int.equal x v -> let p2= Array.make ((Array.length p1)+n) (Pint coef0) in
         for i=0 to (Array.length p1)-1 do
           p2.(i+n)<-p1.(i);
         done;
         Prec (x,p2)
     |_ -> if equal p (Pint coef0) then (Pint coef0)
-       else (let p2=Array.create (n+1) (Pint coef0) in
+       else (let p2=Array.make (n+1) (Pint coef0) in
                p2.(n)<-p;
                Prec (v,p2))
 
@@ -313,14 +306,14 @@ let rec multP p q =
 
 
 (* derive p with variable v, v >= max_var p *)
-let rec deriv v p =
+let deriv v p =
   match p with
       Pint a -> Pint coef0
-    | Prec(x,p1) when x=v ->
+    | Prec(x,p1) when Int.equal x v ->
        let d = Array.length p1 -1 in
-         if d=1 then p1.(1)
+         if Int.equal d 1 then p1.(1)
          else
-           (let p2 = Array.create d (Pint coef0) in
+           (let p2 = Array.make d (Pint coef0) in
               for i=0 to d-1 do
 		p2.(i)<- multP (Pint (coef_of_int (i+1))) p1.(i+1);
               done;
@@ -415,7 +408,7 @@ let rec string_of_Pcut p =
       and s=ref ""
       and sp=ref "" in
     let st0 = string_of_Pcut t.(0) in
-      if st0<>"0"
+      if not (String.equal st0 "0")
       then s:=st0;
     let fin = ref false in
     for i=(Array.length t)-1 downto 1 do
@@ -426,31 +419,31 @@ let rec string_of_Pcut p =
       else (
 	let si=string_of_Pcut  t.(i) in
 	sp:="";
-	if i=1
+	if Int.equal i 1
 	then (
-	  if si<>"0"
+	  if not (String.equal si "0")
 	  then (nsP:=(!nsP)-1;
-		if si="1"
+		if String.equal si "1"
 		then sp:=v
 		else
 		  (if (String.contains si '+')
 		  then sp:="("^si^")*"^v
 		  else sp:=si^"*"^v)))
 	else (
-	  if si<>"0"
+	  if not (String.equal si "0")
 	  then (nsP:=(!nsP)-1;
-		if si="1"
+		if String.equal si "1"
 		then sp:=v^"^"^(string_of_int i)
 		else (if (String.contains si '+')
 		then sp:="("^si^")*"^v^"^"^(string_of_int i)
 		else  sp:=si^"*"^v^"^"^(string_of_int i))));
-	if !sp<>"" && not (!fin)
+	if not (String.is_empty !sp) && not (!fin)
 	then (nsP:=(!nsP)-1;
-	      if !s=""
+	      if String.is_empty !s
 	      then s:=!sp
 	      else s:=(!s)^"+"^(!sp)));
     done;
-    if !s="" then (nsP:=(!nsP)-1;
+    if String.is_empty !s then (nsP:=(!nsP)-1;
 		   (s:="0"));
     !s
 
@@ -473,7 +466,7 @@ let print_lpoly lp = print_tpoly (Array.of_list lp)
 
 (* return (s,r) s.t. p = s*q+r *)
 let rec quo_rem_pol p q x =
-  if x=0
+  if Int.equal x 0
   then (match (p,q) with
           |(Pint a, Pint b) ->
 	     if C.equal (C.modulo a b) coef0
@@ -519,12 +512,11 @@ let divP p q=
 
 let div_pol_rat p q=
   let x = max (max_var_pol p) (max_var_pol q) in
-    try (let s = div_pol (multP p (puisP (Pint(coef_int_tete q))
-				     (1+(deg x p) - (deg x q))))
-		   q x in
-         (* degueulasse, mais c 'est pour enlever un warning *)
-         if s==s then true else true)
-    with e when Errors.noncritical e -> false
+  try
+    let r = puisP (Pint(coef_int_tete q)) (1+(deg x p)-(deg x q)) in
+    let _ = div_pol (multP p r) q x in
+    true
+  with Failure _ -> false
 
 (***********************************************************************
   5. Pseudo-division and gcd with subresultants.
@@ -538,7 +530,7 @@ let div_pol_rat p q=
 let pseudo_div p q x =
   match q with
       Pint _ -> (cf0, q,1, p)
-    | Prec (v,q1) when x<>v -> (cf0, q,1, p)
+    | Prec (v,q1) when not (Int.equal x v) -> (cf0, q,1, p)
     | Prec (v,q1) ->
 	(
 	  (*  pr "pseudo_division: c^d*p = s*q + r";*)
@@ -575,13 +567,13 @@ and pgcd_pol p q x =
 
 and content_pol p x =
   match p with
-      Prec(v,p1) when v=x ->
+      Prec(v,p1) when Int.equal v x ->
         Array.fold_left (fun a b -> pgcd_pol_rec a b (x-1)) cf0 p1
     | _ -> p
 
 and pgcd_coef_pol c p x =
   match p with
-      Prec(v,p1) when x=v ->
+      Prec(v,p1) when Int.equal x v ->
         Array.fold_left (fun a b -> pgcd_pol_rec a b (x-1)) c  p1
     |_ -> pgcd_pol_rec c p (x-1)
 
@@ -593,9 +585,9 @@ and pgcd_pol_rec p q x =
 	  then q
 	  else if equal q cf0
 	  then p
-	  else if (deg x q) = 0
+	  else if Int.equal (deg x q) 0
 	  then pgcd_coef_pol q p x
-	  else if (deg x p) = 0
+	  else if Int.equal (deg x p) 0
 	  then pgcd_coef_pol p q x
 	  else (
 	    let a = content_pol p x in
@@ -610,7 +602,7 @@ and pgcd_pol_rec p q x =
 	    res
 	   )
 
-(* Sub-résultants:
+(* Sub-résultants:
 
    ai*Ai = Qi*Ai+1 + bi*Ai+2
 
@@ -655,7 +647,7 @@ and gcd_sub_res_rec p q s c d x =
 
 and lazard_power c s d x =
   let res = ref c in
-    for i=1 to d-1 do
+    for _i = 1 to d - 1 do
       res:= div_pol ((!res)@@c) s x;
     done;
     !res
diff --git a/plugins/nsatz/polynom.mli b/plugins/nsatz/polynom.mli
index 0f1e0481..9d46cd99 100644
--- a/plugins/nsatz/polynom.mli
+++ b/plugins/nsatz/polynom.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index 17c8654b..8e2fc07c 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -26,20 +26,6 @@ let set_of_list_eq eq l =
    List.iter (fun x -> if not (list_mem_eq eq x (!res)) then res:=x::(!res)) l;
    List.rev !res
 
-
-(* Memoization
-   f is compatible with nf: f(nf(x)) = f(x)
-*)
-
-let memos s memoire nf f x =
-   try (let v = Hashtbl.find memoire (nf x) in pr s;v)
-   with e when Errors.noncritical e ->
-     (pr "#";
-      let v = f x in
-      Hashtbl.add memoire (nf x) v;
-      v)
-
-
 (**********************************************************************
   Eléments minimaux pour un ordre partiel de division.
   E est un ensemble, avec une multiplication
@@ -95,7 +81,7 @@ let facteurs_liste div constant lp =
    c est un élément quelconque de E.
 *)
 let factorise_tableau div zero c f l1 =
-    let res = Array.create (Array.length f) (c,[]) in
+    let res = Array.make (Array.length f) (c,[]) in
     Array.iteri (fun i p ->
       let r = ref p in
       let li = ref [] in
diff --git a/plugins/nsatz/utile.mli b/plugins/nsatz/utile.mli
index 83b2ac39..1f841575 100644
--- a/plugins/nsatz/utile.mli
+++ b/plugins/nsatz/utile.mli
@@ -10,10 +10,6 @@ val info : string -> unit
 val list_mem_eq : ('a -> 'b -> bool) -> 'a -> 'b list -> bool
 val set_of_list_eq : ('a -> 'a -> bool) -> 'a list -> 'a list
 
-(* Memoization *)
-val memos :
-  string -> ('a, 'b) Hashtbl.t -> ('c -> 'a) -> ('c -> 'b) -> 'c -> 'b
-
 
 val facteurs_liste : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a list -> 'a list
 val factorise_tableau :