Micromega: improvement of the code obtained by extraction

  * In eval_cone and simpl_cone, default patterns were leading
    to duplicated computations. Adaptation of RingMicromega.v
    to prevent that.
  * Use the Ocaml builtin types (lists, pairs, bool, etc) and
    remove the useless conversion functions in mutils.ml and alii.
  * andb was extracted to a correctly lazy but ugly match.
    Let's rather use Ocaml's (&&).

  Remain to be done: take advantage of extraction during the build,
   - either directly if we are using plugins, (no dependency issues)
   - or if we compile statically, at least check later that the
     micromega.ml in the archive and the one auto-generated are in sync.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12034 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 292 insertions, 398 deletions

diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index a5ac92db8..b4b40ca73 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -20,4 +20,22 @@ Require Import VarMap.
 Require Import RingMicromega.
 Require Import NArith.
 
-Extraction "micromega.ml"  List.map simpl_cone map_cone indexes  n_of_Z Nnat.N_of_nat ZTautoChecker QTautoChecker find.
+Extract Inductive prod => "( * )" [ "(,)" ].
+Extract Inductive List.list => list [ "[]" "(::)" ].
+Extract Inductive bool => bool [ true false ].
+Extract Inductive sumbool => bool [ true false ].
+Extract Inductive option => option [ Some None ].
+Extract Inductive sumor => option [ Some None ].
+(** Then, in a ternary alternative { }+{ }+{ },
+   -  leftmost choice (Inleft Left) is (Some true),
+   -  middle choice (Inleft Right) is (Some false),
+   -  rightmost choice (Inright) is (None) *)
+
+
+(** To preserve its laziness, andb is normally expansed.
+    Let's rather use the ocaml && *)
+Extract Inlined Constant andb => "(&&)".
+
+Extraction "micromega.ml"
+  List.map simpl_cone map_cone indexes
+  n_of_Z Nnat.N_of_nat ZTautoChecker QTautoChecker find.
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 6885b82cd..c093d7ca0 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -420,9 +420,10 @@ Qed.
 (* Provides the cone member from the witness, i.e., ConeMember *)
 Fixpoint eval_cone (l : list NFormula) (cm : ConeMember) {struct cm} : NFormula :=
 match cm with
-| S_In n => match nth n l (PEc cO, Equal) with
-            | (_, NonEqual) => (PEc cO, Equal)
-            | f => f
+| S_In n => let f := nth n l (PEc cO, Equal) in
+            match f with
+              | (_, NonEqual) => (PEc cO, Equal)
+              | _ => f
             end
 | S_Ideal p cm' => nformula_times_0 p (eval_cone l cm')
 | S_Square p => (PEmul p p, NonStrict)
@@ -746,9 +747,10 @@ Fixpoint simpl_expr (e:PExprC) : PExprC :=
 
 Definition simpl_cone (e:ConeMember) : ConeMember :=
   match e with
-    | S_Square t => match simpl_expr t with
+    | S_Square t => let x:=simpl_expr t in
+                    match x with
                       | PEc c   => if ceqb cO c then S_Z else S_Pos (ctimes c c)
-                      |       x     => S_Square x
+                      | _ => S_Square x
                     end
     | S_Mult t1 t2 => 
       match t1 , t2 with
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index a297c1633..5cce8ff97 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -169,7 +169,7 @@ type 'a number_spec = {
  zero : 'a;
  unit : 'a;
  mult : 'a -> 'a -> 'a;
- eqb  : 'a -> 'a -> Mc.bool
+ eqb  : 'a -> 'a -> bool
 }
 
 let z_spec = {
@@ -455,7 +455,7 @@ let primal l =
 
   let cmp x y = Pervasives.compare (fst x) (fst y) in
 
-   snd (List.fold_right (fun  (p,op) (map,l) -> 
+   snd (List.fold_right (fun  (p,op) (map,l) ->
       let (mp,vect) = vect_of_poly map p in  
       let cstr = {coeffs = List.sort cmp vect; op = op_op op ; cst = minus_num (Poly.get Monomial.const p)} in
 
@@ -505,11 +505,10 @@ let simple_linear_prover to_constant l =
 let linear_prover n_spec l  =
  let li = List.combine l (interval 0 (List.length l -1)) in
  let (l1,l') = List.partition 
-  (fun (x,_) -> if snd' x = Mc.NonEqual then true else false) li in
+  (fun (x,_) -> if snd x = Mc.NonEqual then true else false) li in
  let l' = List.map 
-  (fun (c,i) -> let (Mc.Pair(x,y)) = c in 
-                 match y with 
-                   Mc.NonEqual -> failwith "cannot happen" 
+  (fun ((x,y),i) -> match y with
+                   Mc.NonEqual -> failwith "cannot happen"
                   |  y -> ((dev_form n_spec x, y),i)) l' in
   
   simple_linear_prover n_spec l' 
@@ -566,7 +565,7 @@ let  remove e  l  = List.fold_left (fun l x -> if eq x e then l else x::l) [] l
 
 let candidates sys = 
  let ll = List.fold_right (
-  fun (Mc.Pair(e,k)) r -> 
+  fun (e,k) r ->
    match k with 
     | Mc.NonStrict -> (dev_form z_spec e , Ge)::r
     | Mc.Equal     ->  (dev_form z_spec e , Eq)::r 
@@ -587,7 +586,7 @@ let rec xzlinear_prover planes sys =
   | Some prf -> Some (Mc.RatProof prf)
   | None     -> (* find the candidate with the smallest range *)
      (* Grrr - linear_prover is also calling 'make_linear_system' *)
-     let ll = List.fold_right (fun (Mc.Pair(e,k)) r -> match k with 
+     let ll = List.fold_right (fun (e,k) r -> match k with
        Mc.NonEqual -> r  
       | k -> (dev_form z_spec e , 
              match k with
@@ -623,11 +622,11 @@ let rec xzlinear_prover planes sys =
            (match 
              (*x <= ub ->  x  > ub *)
              linear_prover  z_spec 
-              (Mc.Pair(pplus (pmult (pconst ubd) expr) (popp (pconst  ubn)),
+              ((pplus (pmult (pconst ubd) expr) (popp (pconst  ubn)),
                       Mc.NonStrict) :: sys),
             (* lb <= x  -> lb > x *)
             linear_prover z_spec 
-             (Mc.Pair( pplus  (popp (pmult  (pconst lbd) expr)) (pconst lbn) ,  
+             ((pplus (popp (pmult  (pconst lbd) expr)) (pconst lbn),
                      Mc.NonStrict)::sys) 
             with
              | Some cub , Some clb  ->   
@@ -642,17 +641,17 @@ let rec xzlinear_prover planes sys =
        |  _ -> None
 and zlinear_enum  planes expr clb cub l = 
  if clb >/  cub
- then Some Mc.Nil
- else 
+ then Some []
+ else
   let pexpr = pplus (popp (pconst (Ml2C.bigint (numerator clb)))) expr in
-  let sys' = (Mc.Pair(pexpr, Mc.Equal))::l in
+  let sys' = (pexpr, Mc.Equal)::l in
    (*let enum =  *)
    match xzlinear_prover planes sys' with
     | None -> if debug then print_string "zlp?"; None
     | Some prf -> if debug then print_string "zlp!";
     match zlinear_enum planes expr (clb +/ (Int 1)) cub l with
      | None -> None
-     | Some prfl -> Some (Mc.Cons(prf,prfl))
+     | Some prfl -> Some (prf :: prfl)
 
 let zlinear_prover sys =  
  let candidates = candidates sys in
@@ -745,7 +744,7 @@ let  q_cert_of_pos  pos =
    Axiom_eq i ->  Mc.S_In (Ml2C.nat i)
   | Axiom_le i ->  Mc.S_In (Ml2C.nat i)
   | Axiom_lt i ->  Mc.S_In (Ml2C.nat i)
-  | Monoid l  -> Mc.S_Monoid (Ml2C.list Ml2C.nat l)
+  | Monoid l  -> Mc.S_Monoid (List.map Ml2C.nat l)
   | Rational_eq n | Rational_le n | Rational_lt n -> 
      if compare_num n (Int 0) = 0 then Mc.S_Z else
       Mc.S_Pos (Ml2C.q   n)
@@ -774,7 +773,7 @@ let  z_cert_of_pos  pos =
    Axiom_eq i ->  Mc.S_In (Ml2C.nat i)
   | Axiom_le i ->  Mc.S_In (Ml2C.nat i)
   | Axiom_lt i ->  Mc.S_In (Ml2C.nat i)
-  | Monoid l  -> Mc.S_Monoid (Ml2C.list Ml2C.nat l)
+  | Monoid l  -> Mc.S_Monoid (List.map Ml2C.nat l)
   | Rational_eq n | Rational_le n | Rational_lt n -> 
      if compare_num n (Int 0) = 0 then Mc.S_Z else
       Mc.S_Pos (Ml2C.bigint (big_int_of_num  n))
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 3e88af9f0..6a0e4169c 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -73,14 +73,14 @@ let tt : 'cst cnf = []
 let ff : 'cst cnf = [ [] ]
 
 
-type 'cst mc_cnf = ('cst Micromega.nFormula)  Micromega.list Micromega.list
+type 'cst mc_cnf = ('cst Micromega.nFormula) list list
 
 let cnf (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) (f:'cst formula) = 
- let negate a t = 
-  CoqToCaml.list (fun cl -> CoqToCaml.list (fun x -> (x,t)) cl) (negate a) in
+ let negate a t =
+  List.map (fun cl -> List.map (fun x -> (x,t)) cl) (negate a) in
 
- let normalise a t = 
-     CoqToCaml.list (fun cl -> CoqToCaml.list (fun x -> (x,t)) cl) (normalise a) in
+ let normalise a t =
+     List.map (fun cl -> List.map (fun x -> (x,t)) cl) (normalise a) in
 
  let and_cnf x y = x @ y in
 
@@ -369,7 +369,7 @@ struct
 
  let rec pp_n o x =  output_string o  (string_of_int (CoqToCaml.n x))
 
- let dump_pair t1 t2 dump_t1 dump_t2 (Mc.Pair (x,y)) =
+ let dump_pair t1 t2 dump_t1 dump_t2 (x,y) =
   Term.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|])
 
 
@@ -410,31 +410,24 @@ let parse_q term =
  let rec parse_list parse_elt term = 
   let (i,c) = get_left_construct term in
    match i with
-    | 1 -> Mc.Nil
-    | 2 -> Mc.Cons(parse_elt c.(1), parse_list parse_elt c.(2))
+    | 1 -> []
+    | 2 -> parse_elt c.(1) :: parse_list parse_elt c.(2)
     | i -> raise ParseError
 
 
  let rec dump_list typ dump_elt l =
   match l with
-   | Mc.Nil -> Term.mkApp(Lazy.force coq_nil,[| typ |])
-   | Mc.Cons(e,l) -> Term.mkApp(Lazy.force coq_cons, 
-			       [| typ; dump_elt e;dump_list typ dump_elt l|])
-      
- let rec dump_ml_list typ dump_elt l =
-  match l with
    | [] -> Term.mkApp(Lazy.force coq_nil,[| typ |])
-   | e::l -> Term.mkApp(Lazy.force coq_cons, 
-		       [| typ; dump_elt e;dump_ml_list typ dump_elt l|])
-
+   | e :: l -> Term.mkApp(Lazy.force coq_cons,
+			       [| typ; dump_elt e;dump_list typ dump_elt l|])
 
 
  let pp_list op cl elt o l = 
   let rec _pp  o l = 
    match l with
-    | Mc.Nil -> ()
-    | Mc.Cons(e,Mc.Nil) -> Printf.fprintf o "%a" elt e
-    | Mc.Cons(e,l) -> Printf.fprintf o "%a ,%a" elt e  _pp l in
+    | [] -> ()
+    | [e] -> Printf.fprintf o "%a" elt e
+    | e::l -> Printf.fprintf o "%a ,%a" elt e  _pp l in
    Printf.fprintf o "%s%a%s" op _pp l cl 
 
 
@@ -892,8 +885,6 @@ let rec sig_of_cone = function
  | _  -> []
 
 let same_proof sg cl1 cl2 =
- let cl1 = CoqToCaml.list (fun x -> x) cl1 in
- let cl2 = CoqToCaml.list (fun x -> x) cl2 in
  let rec xsame_proof sg = 
   match sg with
    | [] -> true
@@ -918,20 +909,18 @@ let tags_of_cnf wits cnf =
   Names.Idset.empty wits cnf
 
 
-let find_witness prover  polys1 =
- let l = CoqToCaml.list (fun x -> x) polys1 in
-  try_any prover l
+let find_witness prover polys1 = try_any prover polys1
 
 let rec witness prover   l1 l2 = 
  match l2 with
-  | Micromega.Nil -> Some (Micromega.Nil)
-  | Micromega.Cons(e,l2) -> 
-     match find_witness prover   (Micromega.Cons( e,l1)) with
+  | [] -> Some []
+  | e :: l2 ->
+     match find_witness prover (e::l1) with
       | None -> None
-      | Some w -> 
-	 (match witness prover   l1 l2 with
+      | Some w ->
+	 (match witness prover l1 l2 with
 	  | None -> None
-	  | Some l -> Some (Micromega.Cons (w,l))
+	  | Some l -> Some (w::l)
 	 )
 
 
@@ -1154,14 +1143,14 @@ let witness_list_tags prover l =
 let witness_list prover l = 
  let rec xwitness_list l = 
   match l with
-   | Micromega.Nil -> Some(Micromega.Nil)
-   | Micromega.Cons(e,l) -> 
+   | [] -> Some []
+   | e :: l ->
       match find_witness prover e  with
        | None -> None
-       | Some w -> 
+       | Some w ->
 	  (match xwitness_list l with
 	   | None -> None
-	   | Some l -> Some (Micromega.Cons(w,l))
+	   | Some l -> Some (w :: l)
 	  ) in
   xwitness_list l
 
@@ -1252,7 +1241,7 @@ let micromega_tauto negate normalise spec prover env polys1 polys2  gl =
 
         let (ff',res',ids) = (ff',res',List.map Term.mkVar (ids_of_formula ff')) in
 
-       let res' = dump_ml_list (spec.proof_typ) spec.dump_proof   res' in
+       let res' = dump_list (spec.proof_typ) spec.dump_proof   res' in
         (Tacticals.tclTHENSEQ
           [
            Tactics.generalize ids;
@@ -1285,7 +1274,7 @@ let lift_ratproof prover l =
 
 
 type csdpcert = Sos.positivstellensatz option
-type micromega_polys = (Micromega.q Mc.pExpr, Mc.op1) Micromega.prod list
+type micromega_polys = (Micromega.q Mc.pExpr * Mc.op1) list
 type provername = string * int option
 
 let call_csdpcert provername poly =
@@ -1320,20 +1309,20 @@ let call_csdpcert_q provername poly =
   | None -> None
   | Some cert -> 
      let cert = Certificate.q_cert_of_pos cert in
-      match Mc.qWeakChecker (CamlToCoq.list (fun x -> x) poly)  cert with
-       | Mc.True -> Some cert
-       | Mc.False ->  (print_string "buggy certificate" ; flush stdout) ;None
+     if Mc.qWeakChecker poly cert
+     then Some cert
+     else ((print_string "buggy certificate" ; flush stdout) ;None)
 
 
 let call_csdpcert_z provername poly = 
- let l = List.map (fun (Mc.Pair(e,o)) -> (Mc.Pair(z_to_q_expr e,o))) poly in
+ let l = List.map (fun (e,o) -> (z_to_q_expr e,o)) poly in
   match call_csdpcert provername l with
    | None -> None
    | Some cert -> 
       let cert = Certificate.z_cert_of_pos cert in
-       match Mc.zWeakChecker (CamlToCoq.list (fun x -> x) poly)  cert with
-	| Mc.True -> Some cert
-	| Mc.False ->  (print_string "buggy certificate" ; flush stdout) ;None
+      if Mc.zWeakChecker poly cert
+      then Some cert
+      else ((print_string "buggy certificate" ; flush stdout) ;None)
 
 
 let hyps_of_cone  prf = 
@@ -1342,8 +1331,8 @@ let hyps_of_cone  prf =
     | Mc.S_Pos _ | Mc.S_Z | Mc.S_Square _ -> acc
     | Mc.S_In n -> ISet.add (CoqToCaml.nat n) acc
     | Mc.S_Ideal(_,c) -> xtract  c acc
-    | Mc.S_Monoid Mc.Nil   -> acc
-    | Mc.S_Monoid (Mc.Cons(i,l)) -> xtract (Mc.S_Monoid l) (ISet.add (CoqToCaml.nat i) acc)
+    | Mc.S_Monoid []   -> acc
+    | Mc.S_Monoid (i::l) -> xtract (Mc.S_Monoid l) (ISet.add (CoqToCaml.nat i) acc)
     | Mc.S_Add(e1,e2) |  Mc.S_Mult(e1,e2) -> xtract e1 (xtract e2 acc) in
 
     xtract prf ISet.empty
@@ -1371,7 +1360,6 @@ let hyps_of_pt pt =
       | Mc.RatProof p -> ISet.union acc (translate ofset (hyps_of_cone p))
       | Mc.CutProof(_,_,c,pt) -> xhyps (ofset+1) pt (ISet.union (translate (ofset+1) (hyps_of_cone c)) acc)
       | Mc.EnumProof(_,_,_,c1,c2,l) -> 
-	  let l = CoqToCaml.list (fun x -> x) l in
 	  let s = ISet.union acc (translate (ofset +1) (ISet.union (hyps_of_cone c1) (hyps_of_cone c2))) in
 	    List.fold_left (fun s x -> xhyps (ofset +  1) x s) s l in
     
@@ -1399,7 +1387,7 @@ let linear_prover_Z = {
   hyps    = hyps_of_pt ;
   compact = compact_pt ;
   pp_prf  = pp_proof_term;
-  pp_f    = fun o x -> pp_expr pp_z o (fst' x)
+  pp_f    = fun o x -> pp_expr pp_z o (fst x)
 }
 
 let linear_prover_Q = {
@@ -1408,7 +1396,7 @@ let linear_prover_Q = {
   hyps    = hyps_of_cone ; 
   compact = compact_cone ;
   pp_prf  = pp_cone pp_q ;
-  pp_f   = fun o x -> pp_expr pp_q o  (fst' x)
+  pp_f   = fun o x -> pp_expr pp_q o  (fst x)
 }
 
 let linear_prover_R = {
@@ -1417,7 +1405,7 @@ let linear_prover_R = {
   hyps    = hyps_of_cone ; 
   compact = compact_cone ;
   pp_prf  = pp_cone pp_z ;
-  pp_f    =  fun o x -> pp_expr pp_z o (fst' x)
+  pp_f    =  fun o x -> pp_expr pp_z o (fst x)
 }
 
 let non_linear_prover_Q str o = {
@@ -1426,7 +1414,7 @@ let non_linear_prover_Q str o = {
   hyps    = hyps_of_cone;
   compact = compact_cone ;
   pp_prf  = pp_cone pp_q ;
-  pp_f    = fun o x -> pp_expr pp_q o  (fst' x)
+  pp_f    = fun o x -> pp_expr pp_q o  (fst x)
 }
 
 let non_linear_prover_R str o = {
@@ -1435,7 +1423,7 @@ let non_linear_prover_R str o = {
   hyps    = hyps_of_cone;
   compact = compact_cone;
   pp_prf  = pp_cone pp_z;
-  pp_f    = fun o x -> pp_expr pp_z o  (fst' x)
+  pp_f    = fun o x -> pp_expr pp_z o  (fst x)
 }
 
 let non_linear_prover_Z str o  = {
@@ -1444,7 +1432,7 @@ let non_linear_prover_Z str o  = {
   hyps    = hyps_of_pt;
   compact = compact_pt;
   pp_prf  = pp_proof_term;
-  pp_f    =  fun o x -> pp_expr pp_z o (fst' x)
+  pp_f    =  fun o x -> pp_expr pp_z o (fst x)
 }
 
 let linear_Z =   {
@@ -1453,7 +1441,7 @@ let linear_Z =   {
   hyps   = hyps_of_pt;
   compact = compact_pt;
   pp_prf      = pp_proof_term;
-  pp_f    = fun o x -> pp_expr pp_z o (fst' x)
+  pp_f    = fun o x -> pp_expr pp_z o (fst x)
 }
 
 
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index e151e4e1d..db339ff0d 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -1,27 +1,16 @@
 type __ = Obj.t
 let __ = let rec f _ = Obj.repr f in Obj.repr f
 
-type bool =
-  | True
-  | False
-
 (** val negb : bool -> bool **)
 
 let negb = function
-  | True -> False
-  | False -> True
+  | true -> false
+  | false -> true
 
 type nat =
   | O
   | S of nat
 
-type 'a option =
-  | Some of 'a
-  | None
-
-type ('a, 'b) prod =
-  | Pair of 'a * 'b
-
 type comparison =
   | Eq
   | Lt
@@ -34,42 +23,29 @@ let compOpp = function
   | Lt -> Gt
   | Gt -> Lt
 
-type sumbool =
-  | Left
-  | Right
-
-type 'a sumor =
-  | Inleft of 'a
-  | Inright
-
-type 'a list =
-  | Nil
-  | Cons of 'a * 'a list
-
 (** val app : 'a1 list -> 'a1 list -> 'a1 list **)
 
 let rec app l m =
   match l with
-    | Nil -> m
-    | Cons (a, l1) -> Cons (a, (app l1 m))
+    | [] -> m
+    | a :: l1 -> a :: (app l1 m)
 
 (** val nth : nat -> 'a1 list -> 'a1 -> 'a1 **)
 
 let rec nth n0 l default =
   match n0 with
     | O -> (match l with
-              | Nil -> default
-              | Cons (x, l') -> x)
-    | S m ->
-        (match l with
-           | Nil -> default
-           | Cons (x, t0) -> nth m t0 default)
+              | [] -> default
+              | x :: l' -> x)
+    | S m -> (match l with
+                | [] -> default
+                | x :: t0 -> nth m t0 default)
 
 (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
 
 let rec map f = function
-  | Nil -> Nil
-  | Cons (a, t0) -> Cons ((f a), (map f t0))
+  | [] -> []
+  | a :: t0 -> (f a) :: (map f t0)
 
 type positive =
   | XI of positive
@@ -347,55 +323,53 @@ let zcompare x y =
            | Zneg y' -> compOpp (pcompare x' y' Eq)
            | _ -> Lt)
 
-(** val dcompare_inf : comparison -> sumbool sumor **)
+(** val dcompare_inf : comparison -> bool option **)
 
 let dcompare_inf = function
-  | Eq -> Inleft Left
-  | Lt -> Inleft Right
-  | Gt -> Inright
+  | Eq -> Some true
+  | Lt -> Some false
+  | Gt -> None
 
 (** val zcompare_rec :
     z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 
 let zcompare_rec x y h1 h2 h3 =
   match dcompare_inf (zcompare x y) with
-    | Inleft x0 -> (match x0 with
-                      | Left -> h1 __
-                      | Right -> h2 __)
-    | Inright -> h3 __
+    | Some x0 -> if x0 then h1 __ else h2 __
+    | None -> h3 __
 
-(** val z_gt_dec : z -> z -> sumbool **)
+(** val z_gt_dec : z -> z -> bool **)
 
 let z_gt_dec x y =
-  zcompare_rec x y (fun _ -> Right) (fun _ -> Right) (fun _ -> Left)
+  zcompare_rec x y (fun _ -> false) (fun _ -> false) (fun _ -> true)
 
 (** val zle_bool : z -> z -> bool **)
 
 let zle_bool x y =
   match zcompare x y with
-    | Gt -> False
-    | _ -> True
+    | Gt -> false
+    | _ -> true
 
 (** val zge_bool : z -> z -> bool **)
 
 let zge_bool x y =
   match zcompare x y with
-    | Lt -> False
-    | _ -> True
+    | Lt -> false
+    | _ -> true
 
 (** val zgt_bool : z -> z -> bool **)
 
 let zgt_bool x y =
   match zcompare x y with
-    | Gt -> True
-    | _ -> False
+    | Gt -> true
+    | _ -> false
 
 (** val zeq_bool : z -> z -> bool **)
 
 let zeq_bool x y =
   match zcompare x y with
-    | Eq -> True
-    | _ -> False
+    | Eq -> true
+    | _ -> false
 
 (** val n_of_nat : nat -> n **)
 
@@ -403,54 +377,49 @@ let n_of_nat = function
   | O -> N0
   | S n' -> Npos (p_of_succ_nat n')
 
-(** val zdiv_eucl_POS : positive -> z -> (z, z) prod **)
+(** val zdiv_eucl_POS : positive -> z -> z  *  z **)
 
 let rec zdiv_eucl_POS a b =
   match a with
     | XI a' ->
-        let Pair (q0, r) = zdiv_eucl_POS a' b in
+        let q0 , r = zdiv_eucl_POS a' b in
         let r' = zplus (zmult (Zpos (XO XH)) r) (Zpos XH) in
-        (match zgt_bool b r' with
-           | True -> Pair ((zmult (Zpos (XO XH)) q0), r')
-           | False -> Pair ((zplus (zmult (Zpos (XO XH)) q0) (Zpos XH)),
-               (zminus r' b)))
+        if zgt_bool b r'
+        then (zmult (Zpos (XO XH)) q0) , r'
+        else (zplus (zmult (Zpos (XO XH)) q0) (Zpos XH)) , (zminus r' b)
     | XO a' ->
-        let Pair (q0, r) = zdiv_eucl_POS a' b in
+        let q0 , r = zdiv_eucl_POS a' b in
         let r' = zmult (Zpos (XO XH)) r in
-        (match zgt_bool b r' with
-           | True -> Pair ((zmult (Zpos (XO XH)) q0), r')
-           | False -> Pair ((zplus (zmult (Zpos (XO XH)) q0) (Zpos XH)),
-               (zminus r' b)))
+        if zgt_bool b r'
+        then (zmult (Zpos (XO XH)) q0) , r'
+        else (zplus (zmult (Zpos (XO XH)) q0) (Zpos XH)) , (zminus r' b)
     | XH ->
-        (match zge_bool b (Zpos (XO XH)) with
-           | True -> Pair (Z0, (Zpos XH))
-           | False -> Pair ((Zpos XH), Z0))
+        if zge_bool b (Zpos (XO XH)) then Z0 , (Zpos XH) else (Zpos XH) , Z0
 
-(** val zdiv_eucl : z -> z -> (z, z) prod **)
+(** val zdiv_eucl : z -> z -> z  *  z **)
 
 let zdiv_eucl a b =
   match a with
-    | Z0 -> Pair (Z0, Z0)
+    | Z0 -> Z0 , Z0
     | Zpos a' ->
         (match b with
-           | Z0 -> Pair (Z0, Z0)
+           | Z0 -> Z0 , Z0
            | Zpos p -> zdiv_eucl_POS a' b
            | Zneg b' ->
-               let Pair (q0, r) = zdiv_eucl_POS a' (Zpos b') in
+               let q0 , r = zdiv_eucl_POS a' (Zpos b') in
                (match r with
-                  | Z0 -> Pair ((zopp q0), Z0)
-                  | _ -> Pair ((zopp (zplus q0 (Zpos XH))), (zplus b r))))
+                  | Z0 -> (zopp q0) , Z0
+                  | _ -> (zopp (zplus q0 (Zpos XH))) , (zplus b r)))
     | Zneg a' ->
         (match b with
-           | Z0 -> Pair (Z0, Z0)
+           | Z0 -> Z0 , Z0
            | Zpos p ->
-               let Pair (q0, r) = zdiv_eucl_POS a' b in
+               let q0 , r = zdiv_eucl_POS a' b in
                (match r with
-                  | Z0 -> Pair ((zopp q0), Z0)
-                  | _ -> Pair ((zopp (zplus q0 (Zpos XH))), (zminus b r)))
+                  | Z0 -> (zopp q0) , Z0
+                  | _ -> (zopp (zplus q0 (Zpos XH))) , (zminus b r))
            | Zneg b' ->
-               let Pair (q0, r) = zdiv_eucl_POS a' (Zpos b') in
-               Pair (q0, (zopp r)))
+               let q0 , r = zdiv_eucl_POS a' (Zpos b') in q0 , (zopp r))
 
 type 'c pol =
   | Pc of 'c
@@ -473,24 +442,21 @@ let rec peq ceqb p p' =
   match p with
     | Pc c -> (match p' with
                  | Pc c' -> ceqb c c'
-                 | _ -> False)
+                 | _ -> false)
     | Pinj (j, q0) ->
         (match p' with
            | Pinj (j', q') ->
                (match pcompare j j' Eq with
                   | Eq -> peq ceqb q0 q'
-                  | _ -> False)
-           | _ -> False)
+                  | _ -> false)
+           | _ -> false)
     | PX (p2, i, q0) ->
         (match p' with
            | PX (p'0, i', q') ->
                (match pcompare i i' Eq with
-                  | Eq ->
-                      (match peq ceqb p2 p'0 with
-                         | True -> peq ceqb q0 q'
-                         | False -> False)
-                  | _ -> False)
-           | _ -> False)
+                  | Eq -> if peq ceqb p2 p'0 then peq ceqb q0 q' else false
+                  | _ -> false)
+           | _ -> false)
 
 (** val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol **)
 
@@ -506,18 +472,17 @@ let mkPinj_pred j p =
 let mkPX cO ceqb p i q0 =
   match p with
     | Pc c ->
-        (match ceqb c cO with
-           | True ->
-               (match q0 with
-                  | Pc c0 -> q0
-                  | Pinj (j', q1) -> Pinj ((pplus XH j'), q1)
-                  | PX (p2, p3, p4) -> Pinj (XH, q0))
-           | False -> PX (p, i, q0))
+        if ceqb c cO
+        then (match q0 with
+                | Pc c0 -> q0
+                | Pinj (j', q1) -> Pinj ((pplus XH j'), q1)
+                | PX (p2, p3, p4) -> Pinj (XH, q0))
+        else PX (p, i, q0)
     | Pinj (p2, p3) -> PX (p, i, q0)
     | PX (p', i', q') ->
-        (match peq ceqb q' (p0 cO) with
-           | True -> PX (p', (pplus i' i), q0)
-           | False -> PX (p, i, q0))
+        if peq ceqb q' (p0 cO)
+        then PX (p', (pplus i' i), q0)
+        else PX (p, i, q0)
 
 (** val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol **)
 
@@ -751,12 +716,9 @@ let rec pmulC_aux cO cmul ceqb p c =
     'a1 -> 'a1 pol **)
 
 let pmulC cO cI cmul ceqb p c =
-  match ceqb c cO with
-    | True -> p0 cO
-    | False ->
-        (match ceqb c cI with
-           | True -> p
-           | False -> pmulC_aux cO cmul ceqb p c)
+  if ceqb c cO
+  then p0 cO
+  else if ceqb c cI then p else pmulC_aux cO cmul ceqb p c
 
 (** val pmulI :
     'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol ->
@@ -928,12 +890,12 @@ type 'term' cnf = 'term' clause list
 (** val tt : 'a1 cnf **)
 
 let tt =
-  Nil
+  []
 
 (** val ff : 'a1 cnf **)
 
 let ff =
-  Cons (Nil, Nil)
+  [] :: []
 
 (** val or_clause_cnf : 'a1 clause -> 'a1 cnf -> 'a1 cnf **)
 
@@ -944,8 +906,8 @@ let or_clause_cnf t0 f =
 
 let rec or_cnf f f' =
   match f with
-    | Nil -> tt
-    | Cons (e, rst) -> app (or_cnf rst f') (or_clause_cnf e f')
+    | [] -> tt
+    | e :: rst -> app (or_cnf rst f') (or_clause_cnf e f')
 
 (** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **)
 
@@ -956,62 +918,48 @@ let and_cnf f1 f2 =
     ('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf **)
 
 let rec xcnf normalise0 negate0 pol0 = function
-  | TT -> (match pol0 with
-             | True -> tt
-             | False -> ff)
-  | FF -> (match pol0 with
-             | True -> ff
-             | False -> tt)
+  | TT -> if pol0 then tt else ff
+  | FF -> if pol0 then ff else tt
   | X -> ff
-  | A x -> (match pol0 with
-              | True -> normalise0 x
-              | False -> negate0 x)
+  | A x -> if pol0 then normalise0 x else negate0 x
   | Cj (e1, e2) ->
-      (match pol0 with
-         | True ->
-             and_cnf (xcnf normalise0 negate0 pol0 e1)
-               (xcnf normalise0 negate0 pol0 e2)
-         | False ->
-             or_cnf (xcnf normalise0 negate0 pol0 e1)
-               (xcnf normalise0 negate0 pol0 e2))
+      if pol0
+      then and_cnf (xcnf normalise0 negate0 pol0 e1)
+             (xcnf normalise0 negate0 pol0 e2)
+      else or_cnf (xcnf normalise0 negate0 pol0 e1)
+             (xcnf normalise0 negate0 pol0 e2)
   | D (e1, e2) ->
-      (match pol0 with
-         | True ->
-             or_cnf (xcnf normalise0 negate0 pol0 e1)
-               (xcnf normalise0 negate0 pol0 e2)
-         | False ->
-             and_cnf (xcnf normalise0 negate0 pol0 e1)
-               (xcnf normalise0 negate0 pol0 e2))
+      if pol0
+      then or_cnf (xcnf normalise0 negate0 pol0 e1)
+             (xcnf normalise0 negate0 pol0 e2)
+      else and_cnf (xcnf normalise0 negate0 pol0 e1)
+             (xcnf normalise0 negate0 pol0 e2)
   | N e -> xcnf normalise0 negate0 (negb pol0) e
   | I (e1, e2) ->
-      (match pol0 with
-         | True ->
-             or_cnf (xcnf normalise0 negate0 (negb pol0) e1)
-               (xcnf normalise0 negate0 pol0 e2)
-         | False ->
-             and_cnf (xcnf normalise0 negate0 (negb pol0) e1)
-               (xcnf normalise0 negate0 pol0 e2))
+      if pol0
+      then or_cnf (xcnf normalise0 negate0 (negb pol0) e1)
+             (xcnf normalise0 negate0 pol0 e2)
+      else and_cnf (xcnf normalise0 negate0 (negb pol0) e1)
+             (xcnf normalise0 negate0 pol0 e2)
 
 (** val cnf_checker :
     ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool **)
 
 let rec cnf_checker checker f l =
   match f with
-    | Nil -> True
-    | Cons (e, f0) ->
+    | [] -> true
+    | e :: f0 ->
         (match l with
-           | Nil -> False
-           | Cons (c, l0) ->
-               (match checker e c with
-                  | True -> cnf_checker checker f0 l0
-                  | False -> False))
+           | [] -> false
+           | c :: l0 ->
+               if checker e c then cnf_checker checker f0 l0 else false)
 
 (** val tauto_checker :
     ('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1
     bFormula -> 'a3 list -> bool **)
 
 let tauto_checker normalise0 negate0 checker f w =
-  cnf_checker checker (xcnf normalise0 negate0 True f) w
+  cnf_checker checker (xcnf normalise0 negate0 true f) w
 
 type 'c pExprC = 'c pExpr
 
@@ -1023,7 +971,7 @@ type op1 =
   | Strict
   | NonStrict
 
-type 'c nFormula = ('c pExprC, op1) prod
+type 'c nFormula = 'c pExprC  *  op1
 
 type monoidMember = nat list
 
@@ -1040,36 +988,36 @@ type 'c coneMember =
 (** val nformula_times : 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula **)
 
 let nformula_times f f' =
-  let Pair (p, op) = f in
-  let Pair (p', op') = f' in
-  Pair ((PEmul (p, p')),
+  let p , op = f in
+  let p' , op' = f' in
+  (PEmul (p, p')) ,
   (match op with
      | Equal -> Equal
      | NonEqual -> NonEqual
      | Strict -> op'
-     | NonStrict -> NonStrict))
+     | NonStrict -> NonStrict)
 
 (** val nformula_plus : 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula **)
 
 let nformula_plus f f' =
-  let Pair (p, op) = f in
-  let Pair (p', op') = f' in
-  Pair ((PEadd (p, p')),
+  let p , op = f in
+  let p' , op' = f' in
+  (PEadd (p, p')) ,
   (match op with
      | Equal -> op'
      | NonEqual -> NonEqual
      | Strict -> Strict
      | NonStrict -> (match op' with
                        | Strict -> Strict
-                       | _ -> NonStrict)))
+                       | _ -> NonStrict))
 
 (** val eval_monoid :
     'a1 -> 'a1 nFormula list -> monoidMember -> 'a1 pExprC **)
 
 let rec eval_monoid cI l = function
-  | Nil -> PEc cI
-  | Cons (n0, ns0) -> PEmul
-      ((let Pair (q0, o) = nth n0 l (Pair ((PEc cI), NonEqual)) in
+  | [] -> PEc cI
+  | n0 :: ns0 -> PEmul
+      ((let q0 , o = nth n0 l ((PEc cI) , NonEqual) in
        (match o with
           | NonEqual -> q0
           | _ -> PEc cI)), (eval_monoid cI l ns0))
@@ -1080,18 +1028,19 @@ let rec eval_monoid cI l = function
 
 let rec eval_cone cO cI ceqb cleb l = function
   | S_In n0 ->
-      let Pair (p, o) = nth n0 l (Pair ((PEc cO), Equal)) in
+      let f = nth n0 l ((PEc cO) , Equal) in
+      let p , o = f in
       (match o with
-         | NonEqual -> Pair ((PEc cO), Equal)
-         | _ -> nth n0 l (Pair ((PEc cO), Equal)))
+         | NonEqual -> (PEc cO) , Equal
+         | _ -> f)
   | S_Ideal (p, cm') ->
       let f = eval_cone cO cI ceqb cleb l cm' in
-      let Pair (q0, op) = f in
+      let q0 , op = f in
       (match op with
-         | Equal -> Pair ((PEmul (q0, p)), Equal)
+         | Equal -> (PEmul (q0, p)) , Equal
          | _ -> f)
-  | S_Square p -> Pair ((PEmul (p, p)), NonStrict)
-  | S_Monoid m -> let p = eval_monoid cI l m in Pair ((PEmul (p, p)), Strict)
+  | S_Square p -> (PEmul (p, p)) , NonStrict
+  | S_Monoid m -> let p = eval_monoid cI l m in (PEmul (p, p)) , Strict
   | S_Mult (p, q0) ->
       nformula_times (eval_cone cO cI ceqb cleb l p)
         (eval_cone cO cI ceqb cleb l q0)
@@ -1099,12 +1048,10 @@ let rec eval_cone cO cI ceqb cleb l = function
       nformula_plus (eval_cone cO cI ceqb cleb l p)
         (eval_cone cO cI ceqb cleb l q0)
   | S_Pos c ->
-      (match match cleb cO c with
-               | True -> negb (ceqb cO c)
-               | False -> False with
-         | True -> Pair ((PEc c), Strict)
-         | False -> Pair ((PEc cO), Equal))
-  | S_Z -> Pair ((PEc cO), Equal)
+      if (&&) (cleb cO c) (negb (ceqb cO c))
+      then (PEc c) , Strict
+      else (PEc cO) , Equal
+  | S_Z -> (PEc cO) , Equal
 
 (** val normalise_pexpr :
     'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
@@ -1119,18 +1066,15 @@ let normalise_pexpr cO cI cplus ctimes cminus copp ceqb x =
     -> 'a1 nFormula -> bool **)
 
 let check_inconsistent cO cI cplus ctimes cminus copp ceqb cleb = function
-  | Pair (e, op) ->
+  | e , op ->
       (match normalise_pexpr cO cI cplus ctimes cminus copp ceqb e with
          | Pc c ->
              (match op with
                 | Equal -> negb (ceqb c cO)
-                | NonEqual -> False
+                | NonEqual -> false
                 | Strict -> cleb c cO
-                | NonStrict ->
-                    (match cleb c cO with
-                       | True -> negb (ceqb c cO)
-                       | False -> False))
-         | _ -> False)
+                | NonStrict -> (&&) (cleb c cO) (negb (ceqb c cO)))
+         | _ -> false)
 
 (** val check_normalised_formulas :
     'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
@@ -1168,36 +1112,36 @@ let frhs x = x.frhs
 let xnormalise t0 =
   let { flhs = lhs; fop = o; frhs = rhs } = t0 in
   (match o with
-     | OpEq -> Cons ((Pair ((PEsub (lhs, rhs)), Strict)), (Cons ((Pair
-         ((PEsub (rhs, lhs)), Strict)), Nil)))
-     | OpNEq -> Cons ((Pair ((PEsub (lhs, rhs)), Equal)), Nil)
-     | OpLe -> Cons ((Pair ((PEsub (lhs, rhs)), Strict)), Nil)
-     | OpGe -> Cons ((Pair ((PEsub (rhs, lhs)), Strict)), Nil)
-     | OpLt -> Cons ((Pair ((PEsub (lhs, rhs)), NonStrict)), Nil)
-     | OpGt -> Cons ((Pair ((PEsub (rhs, lhs)), NonStrict)), Nil))
+     | OpEq -> ((PEsub (lhs, rhs)) , Strict) :: (((PEsub (rhs, lhs)) ,
+         Strict) :: [])
+     | OpNEq -> ((PEsub (lhs, rhs)) , Equal) :: []
+     | OpLe -> ((PEsub (lhs, rhs)) , Strict) :: []
+     | OpGe -> ((PEsub (rhs, lhs)) , Strict) :: []
+     | OpLt -> ((PEsub (lhs, rhs)) , NonStrict) :: []
+     | OpGt -> ((PEsub (rhs, lhs)) , NonStrict) :: [])
 
 (** val cnf_normalise : 'a1 formula -> 'a1 nFormula cnf **)
 
 let cnf_normalise t0 =
-  map (fun x -> Cons (x, Nil)) (xnormalise t0)
+  map (fun x -> x :: []) (xnormalise t0)
 
 (** val xnegate : 'a1 formula -> 'a1 nFormula list **)
 
 let xnegate t0 =
   let { flhs = lhs; fop = o; frhs = rhs } = t0 in
   (match o with
-     | OpEq -> Cons ((Pair ((PEsub (lhs, rhs)), Equal)), Nil)
-     | OpNEq -> Cons ((Pair ((PEsub (lhs, rhs)), Strict)), (Cons ((Pair
-         ((PEsub (rhs, lhs)), Strict)), Nil)))
-     | OpLe -> Cons ((Pair ((PEsub (rhs, lhs)), NonStrict)), Nil)
-     | OpGe -> Cons ((Pair ((PEsub (lhs, rhs)), NonStrict)), Nil)
-     | OpLt -> Cons ((Pair ((PEsub (rhs, lhs)), Strict)), Nil)
-     | OpGt -> Cons ((Pair ((PEsub (lhs, rhs)), Strict)), Nil))
+     | OpEq -> ((PEsub (lhs, rhs)) , Equal) :: []
+     | OpNEq -> ((PEsub (lhs, rhs)) , Strict) :: (((PEsub (rhs, lhs)) ,
+         Strict) :: [])
+     | OpLe -> ((PEsub (rhs, lhs)) , NonStrict) :: []
+     | OpGe -> ((PEsub (lhs, rhs)) , NonStrict) :: []
+     | OpLt -> ((PEsub (rhs, lhs)) , Strict) :: []
+     | OpGt -> ((PEsub (lhs, rhs)) , Strict) :: [])
 
 (** val cnf_negate : 'a1 formula -> 'a1 nFormula cnf **)
 
 let cnf_negate t0 =
-  map (fun x -> Cons (x, Nil)) (xnegate t0)
+  map (fun x -> x :: []) (xnegate t0)
 
 (** val simpl_expr :
     'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pExprC -> 'a1 pExprC **)
@@ -1208,9 +1152,9 @@ let rec simpl_expr cI ceqb e = match e with
       let y' = simpl_expr cI ceqb y in
       (match y' with
          | PEc c ->
-             (match ceqb c cI with
-                | True -> simpl_expr cI ceqb z0
-                | False -> PEmul (y', (simpl_expr cI ceqb z0)))
+             if ceqb c cI
+             then simpl_expr cI ceqb z0
+             else PEmul (y', (simpl_expr cI ceqb z0))
          | _ -> PEmul (y', (simpl_expr cI ceqb z0)))
   | _ -> e
 
@@ -1220,12 +1164,10 @@ let rec simpl_expr cI ceqb e = match e with
 
 let simpl_cone cO cI ctimes ceqb e = match e with
   | S_Square t0 ->
-      (match simpl_expr cI ceqb t0 with
-         | PEc c ->
-             (match ceqb cO c with
-                | True -> S_Z
-                | False -> S_Pos (ctimes c c))
-         | _ -> S_Square (simpl_expr cI ceqb t0))
+      let x = simpl_expr cI ceqb t0 in
+      (match x with
+         | PEc c -> if ceqb cO c then S_Z else S_Pos (ctimes c c)
+         | _ -> S_Square x)
   | S_Mult (t1, t2) ->
       (match t1 with
          | S_Mult (x, x0) ->
@@ -1245,9 +1187,7 @@ let simpl_cone cO cI ctimes ceqb e = match e with
                        | _ ->
                            (match t2 with
                               | S_Pos c ->
-                                  (match ceqb cI c with
-                                     | True -> t1
-                                     | False -> S_Mult (t1, t2))
+                                  if ceqb cI c then t1 else S_Mult (t1, t2)
                               | S_Z -> S_Z
                               | _ -> e)))
          | S_Pos c ->
@@ -1259,24 +1199,16 @@ let simpl_cone cO cI ctimes ceqb e = match e with
                            (match x0 with
                               | S_Pos p2 -> S_Mult ((S_Pos (ctimes c p2)), x)
                               | _ ->
-                                  (match ceqb cI c with
-                                     | True -> t2
-                                     | False -> S_Mult (t1, t2))))
+                                  if ceqb cI c then t2 else S_Mult (t1, t2)))
                 | S_Add (y, z0) -> S_Add ((S_Mult ((S_Pos c), y)), (S_Mult
                     ((S_Pos c), z0)))
                 | S_Pos c0 -> S_Pos (ctimes c c0)
                 | S_Z -> S_Z
-                | _ ->
-                    (match ceqb cI c with
-                       | True -> t2
-                       | False -> S_Mult (t1, t2)))
+                | _ -> if ceqb cI c then t2 else S_Mult (t1, t2))
          | S_Z -> S_Z
          | _ ->
              (match t2 with
-                | S_Pos c ->
-                    (match ceqb cI c with
-                       | True -> t1
-                       | False -> S_Mult (t1, t2))
+                | S_Pos c -> if ceqb cI c then t1 else S_Mult (t1, t2)
                 | S_Z -> S_Z
                 | _ -> e))
   | S_Add (t1, t2) ->
@@ -1297,6 +1229,16 @@ let qnum x = x.qnum
 
 let qden x = x.qden
 
+(** val qeq_bool : q -> q -> bool **)
+
+let qeq_bool x y =
+  zeq_bool (zmult x.qnum (Zpos y.qden)) (zmult y.qnum (Zpos x.qden))
+
+(** val qle_bool : q -> q -> bool **)
+
+let qle_bool x y =
+  zle_bool (zmult x.qnum (Zpos y.qden)) (zmult y.qnum (Zpos x.qden))
+
 (** val qplus : q -> q -> q **)
 
 let qplus x y =
@@ -1348,47 +1290,46 @@ let zWeakChecker x x0 =
 let xnormalise0 t0 =
   let { flhs = lhs; fop = o; frhs = rhs } = t0 in
   (match o with
-     | OpEq -> Cons ((Pair ((PEsub (lhs, (PEadd (rhs, (PEc (Zpos XH)))))),
-         NonStrict)), (Cons ((Pair ((PEsub (rhs, (PEadd (lhs, (PEc (Zpos
-         XH)))))), NonStrict)), Nil)))
-     | OpNEq -> Cons ((Pair ((PEsub (lhs, rhs)), Equal)), Nil)
-     | OpLe -> Cons ((Pair ((PEsub (lhs, (PEadd (rhs, (PEc (Zpos XH)))))),
-         NonStrict)), Nil)
-     | OpGe -> Cons ((Pair ((PEsub (rhs, (PEadd (lhs, (PEc (Zpos XH)))))),
-         NonStrict)), Nil)
-     | OpLt -> Cons ((Pair ((PEsub (lhs, rhs)), NonStrict)), Nil)
-     | OpGt -> Cons ((Pair ((PEsub (rhs, lhs)), NonStrict)), Nil))
+     | OpEq -> ((PEsub (lhs, (PEadd (rhs, (PEc (Zpos XH)))))) , NonStrict) ::
+         (((PEsub (rhs, (PEadd (lhs, (PEc (Zpos XH)))))) , NonStrict) :: [])
+     | OpNEq -> ((PEsub (lhs, rhs)) , Equal) :: []
+     | OpLe -> ((PEsub (lhs, (PEadd (rhs, (PEc (Zpos XH)))))) , NonStrict) ::
+         []
+     | OpGe -> ((PEsub (rhs, (PEadd (lhs, (PEc (Zpos XH)))))) , NonStrict) ::
+         []
+     | OpLt -> ((PEsub (lhs, rhs)) , NonStrict) :: []
+     | OpGt -> ((PEsub (rhs, lhs)) , NonStrict) :: [])
 
 (** val normalise : z formula -> z nFormula cnf **)
 
 let normalise t0 =
-  map (fun x -> Cons (x, Nil)) (xnormalise0 t0)
+  map (fun x -> x :: []) (xnormalise0 t0)
 
 (** val xnegate0 : z formula -> z nFormula list **)
 
 let xnegate0 t0 =
   let { flhs = lhs; fop = o; frhs = rhs } = t0 in
   (match o with
-     | OpEq -> Cons ((Pair ((PEsub (lhs, rhs)), Equal)), Nil)
-     | OpNEq -> Cons ((Pair ((PEsub (lhs, (PEadd (rhs, (PEc (Zpos XH)))))),
-         NonStrict)), (Cons ((Pair ((PEsub (rhs, (PEadd (lhs, (PEc (Zpos
-         XH)))))), NonStrict)), Nil)))
-     | OpLe -> Cons ((Pair ((PEsub (rhs, lhs)), NonStrict)), Nil)
-     | OpGe -> Cons ((Pair ((PEsub (lhs, rhs)), NonStrict)), Nil)
-     | OpLt -> Cons ((Pair ((PEsub (rhs, (PEadd (lhs, (PEc (Zpos XH)))))),
-         NonStrict)), Nil)
-     | OpGt -> Cons ((Pair ((PEsub (lhs, (PEadd (rhs, (PEc (Zpos XH)))))),
-         NonStrict)), Nil))
+     | OpEq -> ((PEsub (lhs, rhs)) , Equal) :: []
+     | OpNEq -> ((PEsub (lhs, (PEadd (rhs, (PEc (Zpos XH)))))) , NonStrict)
+         :: (((PEsub (rhs, (PEadd (lhs, (PEc (Zpos XH)))))) , NonStrict) ::
+         [])
+     | OpLe -> ((PEsub (rhs, lhs)) , NonStrict) :: []
+     | OpGe -> ((PEsub (lhs, rhs)) , NonStrict) :: []
+     | OpLt -> ((PEsub (rhs, (PEadd (lhs, (PEc (Zpos XH)))))) , NonStrict) ::
+         []
+     | OpGt -> ((PEsub (lhs, (PEadd (rhs, (PEc (Zpos XH)))))) , NonStrict) ::
+         [])
 
 (** val negate : z formula -> z nFormula cnf **)
 
 let negate t0 =
-  map (fun x -> Cons (x, Nil)) (xnegate0 t0)
+  map (fun x -> x :: []) (xnegate0 t0)
 
 (** val ceiling : z -> z -> z **)
 
 let ceiling a b =
-  let Pair (q0, r) = zdiv_eucl a b in
+  let q0 , r = zdiv_eucl a b in
   (match r with
      | Z0 -> q0
      | _ -> zplus q0 (Zpos XH))
@@ -1402,7 +1343,7 @@ type proofTerm =
 
 let makeLb v q0 =
   let { qnum = n0; qden = d } = q0 in
-  Pair ((PEsub ((PEmul ((PEc (Zpos d)), v)), (PEc n0))), NonStrict)
+  (PEsub ((PEmul ((PEc (Zpos d)), v)), (PEc n0))) , NonStrict
 
 (** val qceiling : q -> z **)
 
@@ -1412,20 +1353,20 @@ let qceiling q0 =
 (** val makeLbCut : z pExprC -> q -> z nFormula **)
 
 let makeLbCut v q0 =
-  Pair ((PEsub (v, (PEc (qceiling q0)))), NonStrict)
+  (PEsub (v, (PEc (qceiling q0)))) , NonStrict
 
-(** val neg_nformula : z nFormula -> (z pExpr, op1) prod **)
+(** val neg_nformula : z nFormula -> z pExpr  *  op1 **)
 
 let neg_nformula = function
-  | Pair (e, o) -> Pair ((PEopp (PEadd (e, (PEc (Zpos XH))))), o)
+  | e , o -> (PEopp (PEadd (e, (PEc (Zpos XH))))) , o
 
 (** val cutChecker :
     z nFormula list -> z pExpr -> q -> zWitness -> z nFormula option **)
 
 let cutChecker l e lb pf =
-  match zWeakChecker (Cons ((neg_nformula (makeLb e lb)), l)) pf with
-    | True -> Some (makeLbCut e lb)
-    | False -> None
+  if zWeakChecker ((neg_nformula (makeLb e lb)) :: l) pf
+  then Some (makeLbCut e lb)
+  else None
 
 (** val zChecker : z nFormula list -> proofTerm -> bool **)
 
@@ -1433,8 +1374,8 @@ let rec zChecker l = function
   | RatProof pf0 -> zWeakChecker l pf0
   | CutProof (e, q0, pf0, rst) ->
       (match cutChecker l e q0 pf0 with
-         | Some c -> zChecker (Cons (c, l)) rst
-         | None -> False)
+         | Some c -> zChecker (c :: l) rst
+         | None -> false)
   | EnumProof (lb, e, ub, pf1, pf2, rst) ->
       (match cutChecker l e lb pf1 with
          | Some n0 ->
@@ -1442,18 +1383,14 @@ let rec zChecker l = function
                 | Some n1 ->
                     let rec label pfs lb0 ub0 =
                       match pfs with
-                        | Nil ->
-                            (match z_gt_dec lb0 ub0 with
-                               | Left -> True
-                               | Right -> False)
-                        | Cons (pf0, rsr) ->
-                            (match zChecker (Cons ((Pair ((PEsub (e, (PEc
-                                     lb0))), Equal)), l)) pf0 with
-                               | True -> label rsr (zplus lb0 (Zpos XH)) ub0
-                               | False -> False)
+                        | [] -> if z_gt_dec lb0 ub0 then true else false
+                        | pf0 :: rsr ->
+                            (&&)
+                              (zChecker (((PEsub (e, (PEc lb0))) , Equal) ::
+                                l) pf0) (label rsr (zplus lb0 (Zpos XH)) ub0)
                     in label rst (qceiling lb) (zopp (qceiling (qopp ub)))
-                | None -> False)
-         | None -> False)
+                | None -> false)
+         | None -> false)
 
 (** val zTautoChecker : z formula bFormula -> proofTerm list -> bool **)
 
@@ -1473,12 +1410,12 @@ let rec map_cone f e = match e with
 (** val indexes : zWitness -> nat list **)
 
 let rec indexes = function
-  | S_In n0 -> Cons (n0, Nil)
+  | S_In n0 -> n0 :: []
   | S_Ideal (e0, cm) -> indexes cm
   | S_Monoid l -> l
   | S_Mult (cm1, cm2) -> app (indexes cm1) (indexes cm2)
   | S_Add (cm1, cm2) -> app (indexes cm1) (indexes cm2)
-  | _ -> Nil
+  | _ -> []
 
 (** val n_of_Z : z -> n **)
 
@@ -1486,16 +1423,6 @@ let n_of_Z = function
   | Zpos p -> Npos p
   | _ -> N0
 
-(** val qeq_bool : q -> q -> bool **)
-
-let qeq_bool p q0 =
-  zeq_bool (zmult p.qnum (Zpos q0.qden)) (zmult q0.qnum (Zpos p.qden))
-
-(** val qle_bool : q -> q -> bool **)
-
-let qle_bool x y =
-  zle_bool (zmult x.qnum (Zpos y.qden)) (zmult y.qnum (Zpos x.qden))
-
 type qWitness = q coneMember
 
 (** val qWeakChecker : q nFormula list -> q coneMember -> bool **)
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index f94f091e8..948391466 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -1,22 +1,11 @@
 type __ = Obj.t
 
-type bool =
-  | True
-  | False
-
 val negb : bool -> bool
 
 type nat =
   | O
   | S of nat
 
-type 'a option =
-  | Some of 'a
-  | None
-
-type ('a, 'b) prod =
-  | Pair of 'a * 'b
-
 type comparison =
   | Eq
   | Lt
@@ -24,18 +13,6 @@ type comparison =
 
 val compOpp : comparison -> comparison
 
-type sumbool =
-  | Left
-  | Right
-
-type 'a sumor =
-  | Inleft of 'a
-  | Inright
-
-type 'a list =
-  | Nil
-  | Cons of 'a * 'a list
-
 val app : 'a1 list -> 'a1 list -> 'a1 list
 
 val nth : nat -> 'a1 list -> 'a1 -> 'a1
@@ -105,11 +82,11 @@ val zmult : z -> z -> z
 
 val zcompare : z -> z -> comparison
 
-val dcompare_inf : comparison -> sumbool sumor
+val dcompare_inf : comparison -> bool option
 
 val zcompare_rec : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 
-val z_gt_dec : z -> z -> sumbool
+val z_gt_dec : z -> z -> bool
 
 val zle_bool : z -> z -> bool
 
@@ -121,9 +98,9 @@ val zeq_bool : z -> z -> bool
 
 val n_of_nat : nat -> n
 
-val zdiv_eucl_POS : positive -> z -> (z, z) prod
+val zdiv_eucl_POS : positive -> z -> z  *  z
 
-val zdiv_eucl : z -> z -> (z, z) prod
+val zdiv_eucl : z -> z -> z  *  z
 
 type 'c pol =
   | Pc of 'c
@@ -257,7 +234,7 @@ type op1 =
   | Strict
   | NonStrict
 
-type 'c nFormula = ('c pExprC, op1) prod
+type 'c nFormula = 'c pExprC  *  op1
 
 type monoidMember = nat list
 
@@ -331,6 +308,10 @@ val qnum : q -> z
 
 val qden : q -> positive
 
+val qeq_bool : q -> q -> bool
+
+val qle_bool : q -> q -> bool
+
 val qplus : q -> q -> q
 
 val qmult : q -> q -> q
@@ -371,7 +352,7 @@ val qceiling : q -> z
 
 val makeLbCut : z pExprC -> q -> z nFormula
 
-val neg_nformula : z nFormula -> (z pExpr, op1) prod
+val neg_nformula : z nFormula -> z pExpr  *  op1
 
 val cutChecker :
   z nFormula list -> z pExpr -> q -> zWitness -> z nFormula option
@@ -386,10 +367,6 @@ val indexes : zWitness -> nat list
 
 val n_of_Z : z -> n
 
-val qeq_bool : q -> q -> bool
-
-val qle_bool : q -> q -> bool
-
 type qWitness = q coneMember
 
 val qWeakChecker : q nFormula list -> q coneMember -> bool
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 03e3999fd..23db2928a 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -14,9 +14,6 @@
 
 let debug = false
 
-let fst' (Micromega.Pair(x,y)) = x
-let snd' (Micromega.Pair(x,y)) = y
-
 let map_option f x = 
   match x with
     | None -> None
@@ -225,11 +222,6 @@ struct
 
  let num x = Num.Big_int (z_big_int x)
 
- let rec list elt l =
-  match l with
-   | Nil -> []
-   | Cons(e,l) -> (elt e)::(list elt l)
-
  let q_to_num {qnum = x ; qden = y} = 
   Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y)))
   
@@ -256,10 +248,6 @@ struct
   else if nt = 0 then N0
   else Npos (positive nt)
 
-
-   
-
-   
  let rec index  n =
   if n=1 then XH
   else if n land 1 = 1 then XI (index (n lsr 1))
@@ -279,8 +267,6 @@ struct
     (List.rev (digits_of_int n))
     (XH)
 
-    
-
  let z x = 
   match compare x 0 with
    | 0 -> Z0
@@ -311,9 +297,6 @@ struct
   {Micromega.qnum = bigint (numerator n) ; 
    Micromega.qden = positive_big_int (denominator n)}
 
-
- let list elt l = List.fold_right (fun x l -> Cons(elt x, l)) l Nil
-
 end
 
 module Cmp =