micromega : more robust generation of proof terms

- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
  (This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)

14 files changed, 914 insertions, 3514 deletions

diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index 6974f8d99..47b6f7c7f 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -30,13 +30,13 @@ Ltac zchange :=
 
 Ltac zchecker_no_abstract := zchange ; vm_compute ; reflexivity.
 
-Ltac zchecker_abstract := abstract (zchange ; vm_cast_no_check (eq_refl true)).
+Ltac zchecker_abstract := zchange ; vm_cast_no_check (eq_refl true).
 
-Ltac zchecker := zchecker_abstract || zchecker_no_abstract .
+Ltac zchecker := zchecker_no_abstract.
 
-Ltac lia := preprocess; xlia ; zchecker.
+Ltac lia := preprocess; xlia zchecker.
                
-Ltac nia := preprocess; xnlia ; zchecker.
+Ltac nia := preprocess; xnlia zchecker.
 
 
 (* Local Variables: *)
diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v
index e3414b849..acd2751a0 100644
--- a/plugins/micromega/Lqa.v
+++ b/plugins/micromega/Lqa.v
@@ -25,23 +25,20 @@ Ltac rchange :=
   apply (QTautoChecker_sound __ff __wit).
 
 Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity.
-Ltac rchecker_abstract   := abstract (rchange ; vm_cast_no_check (eq_refl true)).
+Ltac rchecker_abstract   := rchange ; vm_cast_no_check (eq_refl true).
 
-Ltac rchecker := (rchecker_abstract || rchecker_no_abstract).
+Ltac rchecker := rchecker_no_abstract.
 
 (** Here, lra stands for linear rational arithmetic *)
-Ltac lra := lra_Q ; rchecker.
+Ltac lra := lra_Q  rchecker.
 
 (** Here, nra stands for non-linear rational arithmetic *)
-Ltac nra := xnqa ; rchecker.
+Ltac nra := xnqa  rchecker.
 
 Ltac xpsatz dom d :=
   let tac := lazymatch dom with
   | Q =>
-    (sos_Q || psatz_Q d) ;
-      (* If csdp is not installed, the previous step might not produce any
-    progress: the rest of the tactical will then fail. Hence the 'try'. *)
-      try  rchecker
+    ((sos_Q rchecker) || (psatz_Q d rchecker))
   | _ => fail "Unsupported domain"
   end in tac.
 
diff --git a/plugins/micromega/Lra.v b/plugins/micromega/Lra.v
index 4d9cf22dd..5b97d8ed3 100644
--- a/plugins/micromega/Lra.v
+++ b/plugins/micromega/Lra.v
@@ -26,23 +26,20 @@ Ltac rchange :=
   apply (RTautoChecker_sound __ff __wit).
 
 Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity.
-Ltac rchecker_abstract   := abstract (rchange ; vm_cast_no_check (eq_refl true)).
+Ltac rchecker_abstract   := rchange ; vm_cast_no_check (eq_refl true).
 
-Ltac rchecker := rchecker_abstract || rchecker_no_abstract.
+Ltac rchecker := rchecker_no_abstract.
 
 (** Here, lra stands for linear real arithmetic *)
-Ltac lra := unfold Rdiv in * ;   lra_R ; rchecker.
+Ltac lra := unfold Rdiv in * ;   lra_R  rchecker.
 
 (** Here, nra stands for non-linear real arithmetic *)
-Ltac nra := unfold Rdiv in * ; xnra ; rchecker.
+Ltac nra := unfold Rdiv in * ; xnra  rchecker.
 
 Ltac xpsatz dom d :=
   let tac := lazymatch dom with
   | R =>
-    (sos_R || psatz_R d) ;
-    (* If csdp is not installed, the previous step might not produce any
-    progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try rchecker
+    (sos_R rchecker) || (psatz_R d rchecker)
   | _ => fail "Unsupported domain"
  end in tac.
 
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 0a41af454..d28bb8286 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -50,7 +50,7 @@ Extract Constant Rinv   => "fun x -> 1 / x".
 
 Extraction "micromega.ml"
   List.map simpl_cone (*map_cone  indexes*)
-  denorm Qpower
+  denorm Qpower vm_add
   n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
 
 
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index c81c025a5..8acf0ff88 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -35,16 +35,10 @@ Ltac nia := Lia.nia.
 Ltac xpsatz dom d :=
   let tac := lazymatch dom with
   | Z =>
-    (sos_Z || psatz_Z d) ; Lia.zchecker
+    (sos_Z Lia.zchecker) || (psatz_Z d  Lia.zchecker)
   | R =>
-    (sos_R || psatz_R d) ;
-    (* If csdp is not installed, the previous step might not produce any
-    progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try Lra.rchecker
-  | Q => (sos_Q || psatz_Q d) ;
-    (* If csdp is not installed, the previous step might not produce any
-    progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try  Lqa.rchecker
+    (sos_R Lra.rchecker) || (psatz_R d Lra.rchecker)
+  | Q => (sos_Q Lqa.rchecker) || (psatz_Q d Lqa.rchecker) 
   | _ => fail "Unsupported domain"
   end in tac.
 
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 4981ddb30..2d2c0bc77 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(* <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        *)
@@ -26,6 +26,7 @@ Set Implicit Arguments.
  *)
 
 Section MakeVarMap.
+  
   Variable A : Type.
   Variable default : A.
 
@@ -46,5 +47,29 @@ Section MakeVarMap.
     end.
 
 
-End MakeVarMap.
+  Fixpoint singleton (x:positive) (v : A) : t :=
+    match x with
+    | xH => Leaf v
+    | xO p => Node (singleton p v) default Empty
+    | xI p => Node Empty default (singleton p v)
+    end.
+  
+  Fixpoint vm_add (x: positive) (v : A) (m : t) {struct m} : t :=
+    match m with
+    | Empty   => singleton x v
+    | Leaf vl =>
+      match x with
+      | xH => Leaf v
+      | xO p => Node (singleton p v) vl Empty
+      | xI p => Node Empty vl (singleton p v)
+      end
+    | Node l o r => 
+      match x with
+      | xH => Node l v r
+      | xI p => Node l o (vm_add p v r)
+      | xO p => Node (vm_add p v l) o r
+      end
+    end.
 
+  
+End MakeVarMap.  
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index faf3b3e69..db8cbf231 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -147,6 +147,17 @@ let rec map_atoms fct f =
     | N f -> N(map_atoms fct f)
     | I(f1,o,f2) -> I(map_atoms fct f1, o , map_atoms fct f2)
 
+let rec map_prop fct f =
+  match f with
+    | TT -> TT
+    | FF -> FF
+    | X x -> X (fct x)
+    | A (at,tg,cstr) -> A(at,tg,cstr)
+    | C (f1,f2) -> C(map_prop fct f1, map_prop fct f2)
+    | D (f1,f2) -> D(map_prop fct f1, map_prop fct f2)
+    | N f -> N(map_prop fct f)
+    | I(f1,o,f2) -> I(map_prop fct f1, o , map_prop fct f2)
+
 (**
   * Collect the identifiers of a (string of) implications. Implication labels
   * are inherited from Coq/CoC's higher order dependent type constructor (Pi).
@@ -292,7 +303,8 @@ let rec add_term  t0 = function
   *)
 
 module ISet = Set.Make(Int)
-
+module IMap = Map.Make(Int)
+  
 (**
   * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of
   * elements of m that are at position i0,...,iN.
@@ -371,6 +383,8 @@ struct
   let coq_and = lazy (init_constant "and")
   let coq_or = lazy (init_constant "or")
   let coq_not = lazy (init_constant "not")
+  let coq_not_gl_ref = (Nametab.locate (  Libnames.qualid_of_string "Coq.Init.Logic.not"))
+
   let coq_iff = lazy (init_constant "iff")
   let coq_True = lazy (init_constant "True")
   let coq_False = lazy (init_constant "False")
@@ -949,6 +963,18 @@ struct
     let (env, n) =  _add env 1 v in
      (env, CamlToCoq.idx n)
 
+   let get_rank env v = 
+
+     let rec _get_rank env n =
+       match env with
+       | [] -> raise (Invalid_argument "get_rank")
+      | e::l ->
+         if eq_constr e v
+         then n
+         else  _get_rank l (n+1)  in 
+     _get_rank env 1
+
+       
    let empty = []
 
    let elements env = env
@@ -1173,33 +1199,32 @@ struct
       with e when CErrors.noncritical e -> (X(t),env,tg) in
 
     let is_prop term =
-     let ty   = Typing.unsafe_type_of (Tacmach.pf_env gl) (Tacmach.project gl) term in
-     let sort = Typing.e_sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in
+      let sort  = Retyping.get_sort_of (Tacmach.pf_env gl)  (Tacmach.project gl) term in 
      Term.is_prop_sort sort in
      
     let rec xparse_formula env tg term =
-     match kind_of_term term with
+      match kind_of_term term with
       | App(l,rst) ->
-          (match rst with
-           | [|a;b|] when eq_constr l (Lazy.force coq_and) ->
-               let f,env,tg = xparse_formula env tg a in
-               let g,env, tg = xparse_formula env tg b  in
-               mkformula_binary mkC term f g,env,tg
-           | [|a;b|] when eq_constr l (Lazy.force coq_or) ->
-               let f,env,tg = xparse_formula env tg a in
-               let g,env,tg  = xparse_formula env tg b in
-               mkformula_binary mkD term f g,env,tg
-           | [|a|] when eq_constr l (Lazy.force coq_not) ->
-               let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg)
-           | [|a;b|] when eq_constr l (Lazy.force coq_iff) ->
-               let f,env,tg = xparse_formula env tg a in
-               let g,env,tg = xparse_formula env tg b in
-               mkformula_binary mkIff term f g,env,tg
-           | _ -> parse_atom env tg term)
-      | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b)->
+        (match rst with
+        | [|a;b|] when eq_constr l (Lazy.force coq_and) ->
+          let f,env,tg = xparse_formula env tg a in
+          let g,env, tg = xparse_formula env tg b  in
+          mkformula_binary mkC term f g,env,tg
+        | [|a;b|] when eq_constr l (Lazy.force coq_or) ->
+          let f,env,tg = xparse_formula env tg a in
+          let g,env,tg  = xparse_formula env tg b in
+          mkformula_binary mkD term f g,env,tg
+        | [|a|] when eq_constr l (Lazy.force coq_not) ->
+          let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg)
+        | [|a;b|] when eq_constr l (Lazy.force coq_iff) ->
           let f,env,tg = xparse_formula env tg a in
           let g,env,tg = xparse_formula env tg b in
-          mkformula_binary mkI term f g,env,tg
+          mkformula_binary mkIff term f g,env,tg
+        | _ -> parse_atom env tg term)
+      | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b)->
+        let f,env,tg = xparse_formula env tg a in
+        let g,env,tg = xparse_formula env tg b in
+        mkformula_binary mkI term f g,env,tg
       | _ when eq_constr term (Lazy.force coq_True) -> (TT,env,tg)
       | _ when eq_constr term (Lazy.force coq_False) -> (FF,env,tg)
       | _ when is_prop term -> X(term),env,tg
@@ -1220,12 +1245,214 @@ struct
      | X(t) -> mkApp(Lazy.force coq_X,[|typ ; t|])  in
    xdump f
 
-  (**
-    * Given a conclusion and a list of affectations, rebuild a term prefixed by
-    * the appropriate letins.
-    * TODO: reverse the list of bindings!
-    *)
 
+  let prop_env_of_formula form =
+    let rec doit env = function
+      | TT | FF | A(_,_,_) -> env
+      | X t -> fst (Env.compute_rank_add env t)
+      | C(f1,f2) | D(f1,f2) | I(f1,_,f2) -> 
+        doit (doit env f1) f2
+      | N f -> doit env f in
+    
+    doit [] form
+
+  let var_env_of_formula form =
+
+    let rec vars_of_expr  = function
+      | Mc.PEX n -> ISet.singleton (CoqToCaml.positive n)
+      | Mc.PEc z -> ISet.empty
+      | Mc.PEadd(e1,e2) | Mc.PEmul(e1,e2) | Mc.PEsub(e1,e2) ->
+        ISet.union (vars_of_expr e1) (vars_of_expr e2)
+      | Mc.PEopp e | Mc.PEpow(e,_)-> vars_of_expr e
+    in
+    
+    let vars_of_atom  {Mc.flhs ; Mc.fop; Mc.frhs} =
+      ISet.union (vars_of_expr flhs) (vars_of_expr frhs) in
+      
+    let rec doit = function
+      |  TT | FF | X _ -> ISet.empty
+      | A (a,t,c) -> vars_of_atom a
+      | C(f1,f2) | D(f1,f2) |I (f1,_,f2) -> ISet.union (doit f1) (doit f2)
+      | N f -> doit f in
+
+    doit  form
+    
+
+
+      
+  type 'cst dump_expr =  (* 'cst is the type of the syntactic constants *)
+    {
+      interp_typ : constr; 
+      dump_cst : 'cst -> constr; 
+      dump_add : constr; 
+      dump_sub : constr;
+      dump_opp : constr;
+      dump_mul : constr;
+      dump_pow : constr;
+      dump_pow_arg : Mc.n -> constr;
+      dump_op  : (Mc.op2 * Term.constr) list
+    }
+
+let dump_zexpr = lazy
+  {
+    interp_typ = Lazy.force coq_Z;
+    dump_cst = dump_z;
+    dump_add = Lazy.force coq_Zplus;
+    dump_sub = Lazy.force coq_Zminus;
+    dump_opp = Lazy.force coq_Zopp;
+    dump_mul = Lazy.force coq_Zmult;
+    dump_pow = Lazy.force coq_Zpower;
+    dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n)));
+    dump_op  = List.map (fun (x,y) -> (y,Lazy.force x)) zop_table
+  }
+
+let dump_qexpr = lazy
+  {
+    interp_typ = Lazy.force coq_Q;
+    dump_cst = dump_q;
+    dump_add = Lazy.force coq_Qplus;
+    dump_sub = Lazy.force coq_Qminus;
+    dump_opp = Lazy.force coq_Qopp;
+    dump_mul = Lazy.force coq_Qmult;
+    dump_pow = Lazy.force coq_Qpower;
+    dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n)));
+    dump_op  = List.map (fun (x,y) -> (y,Lazy.force x)) qop_table      
+  }
+
+  let dump_positive_as_R p =
+  let mult = Lazy.force coq_Rmult in
+  let add  = Lazy.force coq_Rplus  in
+
+  let one  = Lazy.force coq_R1    in 
+  let mk_add x y  = mkApp(add,[|x;y|]) in
+  let mk_mult x y = mkApp(mult,[|x;y|]) in
+
+  let two  = mk_add one one in 
+
+  let rec dump_positive p = 
+      match p with
+      | Mc.XH   -> one
+      | Mc.XO p -> mk_mult two (dump_positive p)
+      | Mc.XI p -> mk_add one (mk_mult two (dump_positive p)) in
+
+  dump_positive p
+
+let dump_n_as_R n =
+  let z = CoqToCaml.n n in
+  if z = 0
+  then Lazy.force coq_R0
+  else dump_positive_as_R (CamlToCoq.positive z)
+    
+
+let rec dump_Rcst_as_R cst = 
+  match cst with
+  | Mc.C0 -> Lazy.force coq_R0 
+  | Mc.C1 ->  Lazy.force coq_R1
+  | Mc.CQ q ->  Term.mkApp(Lazy.force coq_IQR, [| dump_q q |])
+  | Mc.CZ z -> Term.mkApp(Lazy.force coq_IZR, [| dump_z z |])
+  | Mc.CPlus(x,y) -> Term.mkApp(Lazy.force coq_Rplus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |])
+  | Mc.CMinus(x,y) -> Term.mkApp(Lazy.force coq_Rminus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |])
+  | Mc.CMult(x,y) -> Term.mkApp(Lazy.force coq_Rmult, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |])
+  | Mc.CInv t -> Term.mkApp(Lazy.force coq_Rinv, [| dump_Rcst_as_R t |])
+  | Mc.COpp t -> Term.mkApp(Lazy.force coq_Ropp, [| dump_Rcst_as_R t |])
+
+
+let dump_rexpr = lazy
+  {
+    interp_typ = Lazy.force coq_R;
+    dump_cst = dump_Rcst_as_R;
+    dump_add = Lazy.force coq_Rplus;
+    dump_sub = Lazy.force coq_Rminus;
+    dump_opp = Lazy.force coq_Ropp;
+    dump_mul = Lazy.force coq_Rmult;
+    dump_pow = Lazy.force coq_Rpower;
+    dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n)));
+    dump_op  = List.map (fun (x,y) -> (y,Lazy.force x)) rop_table      
+  }
+
+
+    
+    
+(** [make_goal_of_formula depxr vars props form] where 
+     - vars is an environment for the arithmetic variables occuring in form
+     - props is an environment for the propositions occuring in form
+    @return a goal where all the variables and propositions of the formula are quantified
+
+*) 
+
+let rec make_goal_of_formula dexpr form =
+
+  let vars_idx =
+    List.mapi (fun i v -> (v, i+1))  (ISet.elements (var_env_of_formula form)) in
+
+  (*  List.iter (fun (v,i) -> Printf.fprintf stdout "var %i has index %i\n" v i) vars_idx ;*)
+  
+  let props     = prop_env_of_formula form in 
+
+  let vars_n  = List.map (fun (_,i) -> (Names.id_of_string (Printf.sprintf "__x%i" i)) , dexpr.interp_typ) vars_idx in 
+  let props_n = List.mapi (fun i _ -> (Names.id_of_string (Printf.sprintf "__p%i" (i+1))) , Term.mkProp) props in 
+
+  let var_name_pos = List.map2 (fun (idx,_) (id,_) -> id,idx) vars_idx vars_n in
+
+  let  dump_expr i e =
+    let rec dump_expr  = function
+    | Mc.PEX n -> mkRel (i+(List.assoc (CoqToCaml.positive n)  vars_idx))
+    | Mc.PEc z -> dexpr.dump_cst z
+    | Mc.PEadd(e1,e2) -> mkApp(dexpr.dump_add,
+                               [| dump_expr e1;dump_expr e2|])
+    | Mc.PEsub(e1,e2) -> mkApp(dexpr.dump_sub,
+                               [| dump_expr  e1;dump_expr  e2|])
+    | Mc.PEopp e -> mkApp(dexpr.dump_opp,
+                          [| dump_expr  e|])
+    | Mc.PEmul(e1,e2) ->  mkApp(dexpr.dump_mul,
+                                [| dump_expr  e1;dump_expr e2|])
+    | Mc.PEpow(e,n) ->  mkApp(dexpr.dump_pow,
+                              [| dump_expr  e; dexpr.dump_pow_arg  n|])
+    in dump_expr e in
+  
+  let mkop op e1 e2 =
+      try
+        Term.mkApp(List.assoc op dexpr.dump_op, [| e1; e2|])
+      with Not_found ->
+        Term.mkApp(Lazy.force coq_Eq,[|dexpr.interp_typ ; e1 ;e2|]) in
+    
+  let dump_cstr i { Mc.flhs ; Mc.fop ; Mc.frhs } =
+    mkop fop (dump_expr i flhs) (dump_expr i frhs) in
+  
+  let rec xdump pi xi f =
+    match f with
+    | TT  -> Lazy.force coq_True
+    | FF  -> Lazy.force coq_False
+    | C(x,y) -> mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|])
+    | D(x,y) -> mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|])
+    | I(x,_,y) -> mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y)
+    | N(x) -> mkArrow (xdump pi xi x) (Lazy.force coq_False)
+    | A(x,_,_) -> dump_cstr xi x
+    | X(t) -> let idx = Env.get_rank props t in
+              mkRel (pi+idx) in 
+  
+  let nb_vars  = List.length vars_n  in
+  let nb_props = List.length props_n in 
+
+  (*  Printf.fprintf stdout "NBProps : %i\n" nb_props ;*)
+  
+  let subst_prop p =
+    let idx = Env.get_rank props p in
+    mkVar (Names.id_of_string (Printf.sprintf "__p%i"  idx)) in 
+
+  let form' = map_prop subst_prop   form in
+
+  (Term.prodn nb_props (List.map (fun (x,y) -> Names.Name x,y) props_n)
+     (Term.prodn nb_vars (List.map (fun (x,y) -> Names.Name x,y) vars_n)
+        (xdump (List.length vars_n) 0  form)),
+   List.rev props_n, List.rev var_name_pos,form')
+    
+  (**
+     * Given a conclusion and a list of affectations, rebuild a term prefixed by
+     * the appropriate letins.
+     * TODO: reverse the list of bindings!
+  *)
+    
   let set l concl =
    let rec xset acc = function
     | [] -> acc
@@ -1290,39 +1517,35 @@ let rec apply_ids t ids =
   | [] -> t
   | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids
 
-let coq_Node = lazy
+let coq_Node = 
  (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")
-let coq_Leaf = lazy
+let coq_Leaf = 
  (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf")
-let coq_Empty = lazy
+let coq_Empty = 
  (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")
 
-let btree_of_array typ a  =
- let size_of_a = Array.length a in
- let semi_size_of_a = size_of_a lsr 1 in
- let node = Lazy.force coq_Node
- and leaf = Lazy.force coq_Leaf
- and empty = Term.mkApp (Lazy.force coq_Empty, [| typ |]) in
- let rec aux n =
-  if n > size_of_a
-  then empty
-  else if  n > semi_size_of_a
-  then Term.mkApp (leaf, [| typ; a.(n-1) |])
-  else Term.mkApp (node, [| typ; aux (2*n); a.(n-1); aux (2*n+1) |])
- in
-  aux 1
-
-let btree_of_array typ a =
- try
-  btree_of_array typ a
- with x when CErrors.noncritical x ->
-  failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x))
-
-let dump_varmap typ env =
- btree_of_array typ (Array.of_list env)
+let coq_VarMap = 
+  (Coqlib.gen_constant_in_modules "VarMap"
+     [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t")
+ 
+
+let rec dump_varmap typ m =
+  match m with
+  | Mc.Empty -> Term.mkApp(coq_Empty,[| typ |])
+  | Mc.Leaf v -> Term.mkApp(coq_Leaf,[| typ; v|])
+  | Mc.Node(l,o,r) -> 
+    Term.mkApp (coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
+
+
+let vm_of_list env =
+  match env with
+  | [] -> Mc.Empty
+  | (d,_)::_ -> 
+    List.fold_left (fun vm (c,i) ->
+      Mc.vm_add d (CamlToCoq.positive i) c vm) Mc.Empty env 
 
 
 let rec pp_varmap o vm =
@@ -1473,10 +1696,10 @@ let topo_sort_constr l = mk_topo_order Termops.dependent l
   *)
 
 let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*) = 
- let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) 0 env in 
+ (* let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *)
  let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in
  let ff  = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
- let vm = dump_varmap (spec.typ) env in
+ let vm = dump_varmap (spec.typ) (vm_of_list env) in
  (* todo : directly generate the proof term - or generalize before conversion? *)
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
    let gl = Tacmach.New.of_old (fun x -> x) gl in
@@ -1486,15 +1709,10 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
     (set
       [
        ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
-       ("__varmap", vm, Term.mkApp
-        (Coqlib.gen_constant_in_modules "VarMap"
-	[["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); 
+       ("__varmap", vm, Term.mkApp( coq_VarMap, [|spec.typ|])); 
        ("__wit", cert, cert_typ)
       ]
       (Tacmach.pf_concl gl))
-   ;
-      Tactics.generalize (topo_sort_constr env) ;
-   Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
   ] 
   end }
 
@@ -1656,6 +1874,7 @@ let rec abstract_wrt_formula f1 f2 =
 
 exception CsdpNotFound
 
+  
 (**
   * This is the core of Micromega: apply the prover, analyze the result and
   * prune unused fomulas, and finally modify the proof state.
@@ -1740,7 +1959,7 @@ let micromega_gen
     (negate:'cst atom -> 'cst mc_cnf)
     (normalise:'cst atom -> 'cst mc_cnf)
     unsat deduce 
-    spec prover =
+    spec dumpexpr prover tac =
  Proofview.Goal.nf_enter { enter = begin fun gl -> 
     let gl = Tacmach.New.of_old (fun x -> x) gl in
     let concl = Tacmach.pf_concl gl in
@@ -1749,16 +1968,39 @@ let micromega_gen
      let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
      let env = Env.elements env in
      let spec = Lazy.force spec in
+     let dumpexpr = Lazy.force dumpexpr in
      
      match micromega_tauto  negate normalise unsat deduce spec prover env hyps concl gl with
      | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness")
      | Some (ids,ff',res') -> 
-      (Tacticals.New.tclTHENLIST
-	[
-	 Tactics.generalize (List.map Term.mkVar ids) ;
-	 micromega_order_change  spec res' 
-	  (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff'
-	])
+       let (arith_goal,props,vars,ff_arith) = make_goal_of_formula dumpexpr ff' in
+       let intro (id,_) = Tactics.introduction id  in 
+
+       let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
+       let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
+       let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
+       let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in
+       let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in 
+
+       let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
+                                                    micromega_order_change spec res'
+                                                      (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in
+
+       let kill_arith = 
+           Tacticals.New.tclTHEN
+             (Tactics.keep [])
+             ((*Tactics.tclABSTRACT  None*)
+                (Tacticals.New.tclTHEN tac_arith tac)) in 
+
+       Tacticals.New.tclTHEN
+         (Tactics.forward true (Some (Some kill_arith)) (ipat_of_name goal_name) arith_goal)
+         (Tacticals.New.tclTHENLIST
+            [(Tactics.generalize (List.map Term.mkVar ids));
+                Tactics.unfold_constr coq_not_gl_ref;
+                (Tactics.apply (Term.applist (Term.mkVar goal_name,List.rev (prop_env_of_formula ff'))))
+            ])
+                (*Tacticals.New.tclTRY(Tactics.apply_with_bindings_gen true false
+                  [None,(Loc.ghost,((Term.mkVar goal_name) ,Misctypes.NoBindings))]*)
     with
     | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
     | Mfourier.TimeOut  -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
@@ -1780,16 +2022,16 @@ let micromega_gen parse_arith
        
 
 let micromega_order_changer cert env ff  = 
- let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) 0 env in 
- let coeff = Lazy.force coq_Rcst in
- let dump_coeff = dump_Rcst in
- let typ  = Lazy.force coq_R in
- let cert_typ = (Term.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in
+  (*let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *)
+  let coeff = Lazy.force coq_Rcst in
+  let dump_coeff = dump_Rcst in
+  let typ  = Lazy.force coq_R in
+  let cert_typ = (Term.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in
  
- let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
- let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
- let vm = dump_varmap (typ) env in
- Proofview.Goal.nf_enter { enter = begin fun gl -> 
+  let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
+  let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
+  let vm = dump_varmap (typ) (vm_of_list env) in
+  Proofview.Goal.nf_enter { enter = begin fun gl -> 
     let gl = Tacmach.New.of_old (fun x -> x) gl in
     Tacticals.New.tclTHENLIST
      [
@@ -1803,13 +2045,11 @@ let micromega_order_changer cert env ff  =
          ("__wit", cert, cert_typ)
         ]
         (Tacmach.pf_concl gl)));
-      Tactics.generalize (topo_sort_constr env) ;
-      Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
+     (*      Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)*)
      ]
   end }
 
-
-let micromega_genr prover =
+let micromega_genr prover tac =
   let parse_arith = parse_rarith in
   let negate = Mc.rnegate in
   let normalise = Mc.rnormalise in
@@ -1826,6 +2066,7 @@ let micromega_genr prover =
      let gl = Tacmach.New.of_old (fun x -> x) gl in
      let concl = Tacmach.pf_concl gl in
      let hyps  = Tacmach.pf_hyps_types gl in
+
      try
       let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
        let env = Env.elements env in
@@ -1837,23 +2078,51 @@ let micromega_genr prover =
        match micromega_tauto  negate normalise unsat deduce spec prover env hyps' concl' gl with
        | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") 
        | Some (ids,ff',res') -> 
-           let (ff,ids') = formula_hyps_concl 
+         let (ff,ids) = formula_hyps_concl 
 	     (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in
-           (Tacticals.New.tclTHENLIST
-              [
-                Tactics.generalize (List.map Term.mkVar ids) ;
-                micromega_order_changer res' env (abstract_wrt_formula ff' ff)
-              ])
-  with
-  | Mfourier.TimeOut     -> Tacticals.New.tclFAIL 0 (Pp.str "TimeOut")
-  | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
-  | CsdpNotFound ->
-      Tacticals.New.tclFAIL 0 (Pp.str 
-      (" Skipping what remains of this tactic: the complexity of the goal requires "
-      ^ "the use of a specialized external tool called csdp. \n\n" 
-      ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
-       ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
-    end }
+         let ff' = abstract_wrt_formula ff' ff  in
+
+         let (arith_goal,props,vars,ff_arith) = make_goal_of_formula (Lazy.force dump_rexpr)  ff' in
+         let intro (id,_) = Tactics.introduction id  in 
+
+       let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
+       let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
+       let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
+       let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in
+       let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in 
+       
+       let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
+                                                    micromega_order_changer res' env' ff_arith ] in
+
+       let kill_arith = 
+         Tacticals.New.tclTHEN
+           (Tactics.keep [])
+           ((*Tactics.tclABSTRACT  None*)
+             (Tacticals.New.tclTHEN tac_arith tac)) in 
+
+
+       Tacticals.New.tclTHEN
+         (Tactics.forward true (Some (Some kill_arith)) (ipat_of_name goal_name) arith_goal)
+        
+         (Tacticals.New.tclTHENLIST
+               [(Tactics.generalize (List.map Term.mkVar ids));
+                Tactics.unfold_constr coq_not_gl_ref;
+                (Tactics.apply (Term.applist (Term.mkVar goal_name,List.rev (prop_env_of_formula ff'))))
+               ]
+         )
+
+    with
+    | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
+    | Mfourier.TimeOut  -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
+    | CsdpNotFound -> flush stdout ;
+     Tacticals.New.tclFAIL 0 (Pp.str 
+                           (" Skipping what remains of this tactic: the complexity of the goal requires "
+                            ^ "the use of a specialized external tool called csdp. \n\n" 
+                            ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
+                            ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
+  end }
+
+
 
 
 let micromega_genr prover  = (micromega_genr prover)
@@ -2129,11 +2398,11 @@ let tauto_lia ff =
   *)
 
 let lra_Q =
- micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr
   [ linear_prover_Q ] 
 
 let psatz_Q i  =
- micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr
   [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ]
 
 let lra_R  =
@@ -2144,15 +2413,15 @@ let psatz_R i  =
 
 
 let psatz_Z i  =
-    micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
+    micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr
       [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] 
 
 let sos_Z  =
- micromega_gen parse_zarith Mc.negate Mc.normalise  Mc.zunsat Mc.zdeduce zz_domain_spec
+ micromega_gen parse_zarith Mc.negate Mc.normalise  Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr
   [ non_linear_prover_Z "pure_sos" None ] 
 
 let sos_Q  =
- micromega_gen parse_qarith Mc.qnegate Mc.qnormalise  Mc.qunsat Mc.qdeduce qq_domain_spec
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise  Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr
   [ non_linear_prover_Q "pure_sos" None ] 
 
 
@@ -2160,18 +2429,18 @@ let sos_R  =
  micromega_genr  [ non_linear_prover_R "pure_sos" None ] 
 
 
-let xlia  =  micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
+let xlia  =  micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr
       [ linear_Z ] 
 
 let xnlia  =
-    micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
+    micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr
       [ nlinear_Z ] 
 
 let nra  = 
  micromega_genr  [ nlinear_prover_R ] 
 
 let nqa  =
- micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr
   [ nlinear_prover_R ]
 
    
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 974dcee87..027f690fc 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -20,56 +20,64 @@ open Constrarg
 
 DECLARE PLUGIN "micromega_plugin"
 
+TACTIC EXTEND RED
+| [ "myred"  ] -> [ Tactics.red_in_concl ]
+END
+
+
+
 TACTIC EXTEND PsatzZ
-| [ "psatz_Z" int_or_var(i) ] -> [  (Coq_micromega.psatz_Z i) ]
-| [ "psatz_Z" ] -> [  (Coq_micromega.psatz_Z (-1)) ]
+| [ "psatz_Z" int_or_var(i) tactic(t) ] -> [  (Coq_micromega.psatz_Z i
+                                               (Tacinterp.tactic_of_value ist t))
+                                               ]
+| [ "psatz_Z" tactic(t)] -> [  (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) ]
 END
 
 TACTIC EXTEND Lia
-[ "xlia"  ] -> [   (Coq_micromega.xlia) ]
+[ "xlia" tactic(t) ] -> [   (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) ]
 END
 
 TACTIC EXTEND Nia
-[ "xnlia"  ] -> [  (Coq_micromega.xnlia) ]
+[ "xnlia" tactic(t) ] -> [  (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) ]
 END
 
 TACTIC EXTEND NRA
-[ "xnra"  ] -> [  (Coq_micromega.nra)]
+[ "xnra" tactic(t) ] -> [  (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))]
 END
 
 TACTIC EXTEND NQA
-[ "xnqa"  ] -> [  (Coq_micromega.nqa)]
+[ "xnqa" tactic(t) ] -> [  (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))]
 END
 
 
   
 TACTIC EXTEND Sos_Z
-| [ "sos_Z" ] -> [ (Coq_micromega.sos_Z) ]
+| [ "sos_Z" tactic(t) ] -> [ (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) ]
    END
 
 TACTIC EXTEND Sos_Q
-| [ "sos_Q" ] -> [   (Coq_micromega.sos_Q) ]
+| [ "sos_Q" tactic(t) ] -> [   (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) ]
    END
 
 TACTIC EXTEND Sos_R
-| [ "sos_R" ] -> [   (Coq_micromega.sos_R) ]
+| [ "sos_R" tactic(t) ] -> [   (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) ]
 END
 
 TACTIC EXTEND LRA_Q
-[ "lra_Q"  ] -> [   (Coq_micromega.lra_Q) ]
+[ "lra_Q"  tactic(t) ] -> [   (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) ]
 END
 
 TACTIC EXTEND LRA_R
-[ "lra_R"  ] -> [   (Coq_micromega.lra_R) ]
+[ "lra_R" tactic(t) ] -> [   (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) ]
 END
 
 TACTIC EXTEND PsatzR
-| [ "psatz_R" int_or_var(i) ] -> [   (Coq_micromega.psatz_R i) ]
-| [ "psatz_R" ] -> [   (Coq_micromega.psatz_R (-1)) ]
+| [ "psatz_R" int_or_var(i) tactic(t) ] -> [   (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) ]
+| [ "psatz_R" tactic(t) ] -> [   (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) ]
 END
 
 TACTIC EXTEND PsatzQ
-| [ "psatz_Q" int_or_var(i) ] -> [  (Coq_micromega.psatz_Q i) ]
-| [ "psatz_Q" ] -> [  (Coq_micromega.psatz_Q (-1)) ]
+| [ "psatz_Q" int_or_var(i) tactic(t) ] -> [  (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) ]
+| [ "psatz_Q" tactic(t) ] -> [  (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) ]
 END
 
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index 0537cdbe8..5cf1da8ea 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -1,6 +1,3 @@
-type __ = Obj.t
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-
 (** val negb : bool -> bool **)
 
 let negb = function
@@ -11,16 +8,6 @@ type nat =
 | O
 | S of nat
 
-(** val fst : ('a1 * 'a2) -> 'a1 **)
-
-let fst = function
-| x,y -> x
-
-(** val snd : ('a1 * 'a2) -> 'a2 **)
-
-let snd = function
-| x,y -> y
-
 (** val app : 'a1 list -> 'a1 list -> 'a1 list **)
 
 let rec app l m =
@@ -40,42 +27,15 @@ let compOpp = function
 | Lt -> Gt
 | Gt -> Lt
 
-type compareSpecT =
-| CompEqT
-| CompLtT
-| CompGtT
-
-(** val compareSpec2Type : comparison -> compareSpecT **)
-
-let compareSpec2Type = function
-| Eq -> CompEqT
-| Lt -> CompLtT
-| Gt -> CompGtT
-
-type 'a compSpecT = compareSpecT
-
-(** val compSpec2Type : 'a1 -> 'a1 -> comparison -> 'a1 compSpecT **)
-
-let compSpec2Type x y c =
-  compareSpec2Type c
-
-type 'a sig0 =
-  'a
-  (* singleton inductive, whose constructor was exist *)
-
-(** val plus : nat -> nat -> nat **)
-
-let rec plus n0 m =
-  match n0 with
-  | O -> m
-  | S p -> S (plus p m)
-
-(** val nat_iter : nat -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
+module Coq__1 = struct
+ (** val add : nat -> nat -> nat **)
+ let rec add n0 m =
+   match n0 with
+   | O -> m
+   | S p -> S (add p m)
+end
+let add = Coq__1.add
 
-let rec nat_iter n0 f x =
-  match n0 with
-  | O -> x
-  | S n' -> f (nat_iter n' f x)
 
 type positive =
 | XI of positive
@@ -91,592 +51,25 @@ type z =
 | Zpos of positive
 | Zneg of positive
 
-module type TotalOrder' = 
- sig 
-  type t 
- end
-
-module MakeOrderTac = 
- functor (O:TotalOrder') ->
- struct 
-  
- end
-
-module MaxLogicalProperties = 
- functor (O:TotalOrder') ->
- functor (M:sig 
-  val max : O.t -> O.t -> O.t
- end) ->
- struct 
-  module T = MakeOrderTac(O)
- end
-
-module Pos = 
- struct 
-  type t = positive
-  
-  (** val succ : positive -> positive **)
-  
-  let rec succ = function
-  | XI p -> XO (succ p)
-  | XO p -> XI p
-  | XH -> XO XH
-  
-  (** val add : positive -> positive -> positive **)
-  
-  let rec add x y =
-    match x with
-    | XI p ->
-      (match y with
-       | XI q0 -> XO (add_carry p q0)
-       | XO q0 -> XI (add p q0)
-       | XH -> XO (succ p))
-    | XO p ->
-      (match y with
-       | XI q0 -> XI (add p q0)
-       | XO q0 -> XO (add p q0)
-       | XH -> XI p)
-    | XH ->
-      (match y with
-       | XI q0 -> XO (succ q0)
-       | XO q0 -> XI q0
-       | XH -> XO XH)
-  
-  (** val add_carry : positive -> positive -> positive **)
-  
-  and add_carry x y =
-    match x with
-    | XI p ->
-      (match y with
-       | XI q0 -> XI (add_carry p q0)
-       | XO q0 -> XO (add_carry p q0)
-       | XH -> XI (succ p))
-    | XO p ->
-      (match y with
-       | XI q0 -> XO (add_carry p q0)
-       | XO q0 -> XI (add p q0)
-       | XH -> XO (succ p))
-    | XH ->
-      (match y with
-       | XI q0 -> XI (succ q0)
-       | XO q0 -> XO (succ q0)
-       | XH -> XI XH)
-  
-  (** val pred_double : positive -> positive **)
-  
-  let rec pred_double = function
-  | XI p -> XI (XO p)
-  | XO p -> XI (pred_double p)
-  | XH -> XH
-  
-  (** val pred : positive -> positive **)
-  
-  let pred = function
-  | XI p -> XO p
-  | XO p -> pred_double p
-  | XH -> XH
-  
-  (** val pred_N : positive -> n **)
-  
-  let pred_N = function
-  | XI p -> Npos (XO p)
-  | XO p -> Npos (pred_double p)
-  | XH -> N0
-  
+module Pos =
+ struct
   type mask =
   | IsNul
   | IsPos of positive
   | IsNeg
-  
-  (** val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 **)
-  
-  let mask_rect f f0 f1 = function
-  | IsNul -> f
-  | IsPos x -> f0 x
-  | IsNeg -> f1
-  
-  (** val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 **)
-  
-  let mask_rec f f0 f1 = function
-  | IsNul -> f
-  | IsPos x -> f0 x
-  | IsNeg -> f1
-  
-  (** val succ_double_mask : mask -> mask **)
-  
-  let succ_double_mask = function
-  | IsNul -> IsPos XH
-  | IsPos p -> IsPos (XI p)
-  | IsNeg -> IsNeg
-  
-  (** val double_mask : mask -> mask **)
-  
-  let double_mask = function
-  | IsPos p -> IsPos (XO p)
-  | x0 -> x0
-  
-  (** val double_pred_mask : positive -> mask **)
-  
-  let double_pred_mask = function
-  | XI p -> IsPos (XO (XO p))
-  | XO p -> IsPos (XO (pred_double p))
-  | XH -> IsNul
-  
-  (** val pred_mask : mask -> mask **)
-  
-  let pred_mask = function
-  | IsPos q0 ->
-    (match q0 with
-     | XH -> IsNul
-     | _ -> IsPos (pred q0))
-  | _ -> IsNeg
-  
-  (** val sub_mask : positive -> positive -> mask **)
-  
-  let rec sub_mask x y =
-    match x with
-    | XI p ->
-      (match y with
-       | XI q0 -> double_mask (sub_mask p q0)
-       | XO q0 -> succ_double_mask (sub_mask p q0)
-       | XH -> IsPos (XO p))
-    | XO p ->
-      (match y with
-       | XI q0 -> succ_double_mask (sub_mask_carry p q0)
-       | XO q0 -> double_mask (sub_mask p q0)
-       | XH -> IsPos (pred_double p))
-    | XH ->
-      (match y with
-       | XH -> IsNul
-       | _ -> IsNeg)
-  
-  (** val sub_mask_carry : positive -> positive -> mask **)
-  
-  and sub_mask_carry x y =
-    match x with
-    | XI p ->
-      (match y with
-       | XI q0 -> succ_double_mask (sub_mask_carry p q0)
-       | XO q0 -> double_mask (sub_mask p q0)
-       | XH -> IsPos (pred_double p))
-    | XO p ->
-      (match y with
-       | XI q0 -> double_mask (sub_mask_carry p q0)
-       | XO q0 -> succ_double_mask (sub_mask_carry p q0)
-       | XH -> double_pred_mask p)
-    | XH -> IsNeg
-  
-  (** val sub : positive -> positive -> positive **)
-  
-  let sub x y =
-    match sub_mask x y with
-    | IsPos z0 -> z0
-    | _ -> XH
-  
-  (** val mul : positive -> positive -> positive **)
-  
-  let rec mul x y =
-    match x with
-    | XI p -> add y (XO (mul p y))
-    | XO p -> XO (mul p y)
-    | XH -> y
-  
-  (** val iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
-  
-  let rec iter n0 f x =
-    match n0 with
-    | XI n' -> f (iter n' f (iter n' f x))
-    | XO n' -> iter n' f (iter n' f x)
-    | XH -> f x
-  
-  (** val pow : positive -> positive -> positive **)
-  
-  let pow x y =
-    iter y (mul x) XH
-  
-  (** val div2 : positive -> positive **)
-  
-  let div2 = function
-  | XI p2 -> p2
-  | XO p2 -> p2
-  | XH -> XH
-  
-  (** val div2_up : positive -> positive **)
-  
-  let div2_up = function
-  | XI p2 -> succ p2
-  | XO p2 -> p2
-  | XH -> XH
-  
-  (** val size_nat : positive -> nat **)
-  
-  let rec size_nat = function
-  | XI p2 -> S (size_nat p2)
-  | XO p2 -> S (size_nat p2)
-  | XH -> S O
-  
-  (** val size : positive -> positive **)
-  
-  let rec size = function
-  | XI p2 -> succ (size p2)
-  | XO p2 -> succ (size p2)
-  | XH -> XH
-  
-  (** val compare_cont : positive -> positive -> comparison -> comparison **)
-  
-  let rec compare_cont x y r =
-    match x with
-    | XI p ->
-      (match y with
-       | XI q0 -> compare_cont p q0 r
-       | XO q0 -> compare_cont p q0 Gt
-       | XH -> Gt)
-    | XO p ->
-      (match y with
-       | XI q0 -> compare_cont p q0 Lt
-       | XO q0 -> compare_cont p q0 r
-       | XH -> Gt)
-    | XH ->
-      (match y with
-       | XH -> r
-       | _ -> Lt)
-  
-  (** val compare : positive -> positive -> comparison **)
-  
-  let compare x y =
-    compare_cont x y Eq
-  
-  (** val min : positive -> positive -> positive **)
-  
-  let min p p' =
-    match compare p p' with
-    | Gt -> p'
-    | _ -> p
-  
-  (** val max : positive -> positive -> positive **)
-  
-  let max p p' =
-    match compare p p' with
-    | Gt -> p
-    | _ -> p'
-  
-  (** val eqb : positive -> positive -> bool **)
-  
-  let rec eqb p q0 =
-    match p with
-    | XI p2 ->
-      (match q0 with
-       | XI q1 -> eqb p2 q1
-       | _ -> false)
-    | XO p2 ->
-      (match q0 with
-       | XO q1 -> eqb p2 q1
-       | _ -> false)
-    | XH ->
-      (match q0 with
-       | XH -> true
-       | _ -> false)
-  
-  (** val leb : positive -> positive -> bool **)
-  
-  let leb x y =
-    match compare x y with
-    | Gt -> false
-    | _ -> true
-  
-  (** val ltb : positive -> positive -> bool **)
-  
-  let ltb x y =
-    match compare x y with
-    | Lt -> true
-    | _ -> false
-  
-  (** val sqrtrem_step :
-      (positive -> positive) -> (positive -> positive) -> (positive * mask)
-      -> positive * mask **)
-  
-  let sqrtrem_step f g = function
-  | s,y ->
-    (match y with
-     | IsPos r ->
-       let s' = XI (XO s) in
-       let r' = g (f r) in
-       if leb s' r' then (XI s),(sub_mask r' s') else (XO s),(IsPos r')
-     | _ -> (XO s),(sub_mask (g (f XH)) (XO (XO XH))))
-  
-  (** val sqrtrem : positive -> positive * mask **)
-  
-  let rec sqrtrem = function
-  | XI p2 ->
-    (match p2 with
-     | XI p3 -> sqrtrem_step (fun x -> XI x) (fun x -> XI x) (sqrtrem p3)
-     | XO p3 -> sqrtrem_step (fun x -> XO x) (fun x -> XI x) (sqrtrem p3)
-     | XH -> XH,(IsPos (XO XH)))
-  | XO p2 ->
-    (match p2 with
-     | XI p3 -> sqrtrem_step (fun x -> XI x) (fun x -> XO x) (sqrtrem p3)
-     | XO p3 -> sqrtrem_step (fun x -> XO x) (fun x -> XO x) (sqrtrem p3)
-     | XH -> XH,(IsPos XH))
-  | XH -> XH,IsNul
-  
-  (** val sqrt : positive -> positive **)
-  
-  let sqrt p =
-    fst (sqrtrem p)
-  
-  (** val gcdn : nat -> positive -> positive -> positive **)
-  
-  let rec gcdn n0 a b =
-    match n0 with
-    | O -> XH
-    | S n1 ->
-      (match a with
-       | XI a' ->
-         (match b with
-          | XI b' ->
-            (match compare a' b' with
-             | Eq -> a
-             | Lt -> gcdn n1 (sub b' a') a
-             | Gt -> gcdn n1 (sub a' b') b)
-          | XO b0 -> gcdn n1 a b0
-          | XH -> XH)
-       | XO a0 ->
-         (match b with
-          | XI p -> gcdn n1 a0 b
-          | XO b0 -> XO (gcdn n1 a0 b0)
-          | XH -> XH)
-       | XH -> XH)
-  
-  (** val gcd : positive -> positive -> positive **)
-  
-  let gcd a b =
-    gcdn (plus (size_nat a) (size_nat b)) a b
-  
-  (** val ggcdn :
-      nat -> positive -> positive -> positive * (positive * positive) **)
-  
-  let rec ggcdn n0 a b =
-    match n0 with
-    | O -> XH,(a,b)
-    | S n1 ->
-      (match a with
-       | XI a' ->
-         (match b with
-          | XI b' ->
-            (match compare a' b' with
-             | Eq -> a,(XH,XH)
-             | Lt ->
-               let g,p = ggcdn n1 (sub b' a') a in
-               let ba,aa = p in g,(aa,(add aa (XO ba)))
-             | Gt ->
-               let g,p = ggcdn n1 (sub a' b') b in
-               let ab,bb = p in g,((add bb (XO ab)),bb))
-          | XO b0 ->
-            let g,p = ggcdn n1 a b0 in let aa,bb = p in g,(aa,(XO bb))
-          | XH -> XH,(a,XH))
-       | XO a0 ->
-         (match b with
-          | XI p ->
-            let g,p2 = ggcdn n1 a0 b in let aa,bb = p2 in g,((XO aa),bb)
-          | XO b0 -> let g,p = ggcdn n1 a0 b0 in (XO g),p
-          | XH -> XH,(a,XH))
-       | XH -> XH,(XH,b))
-  
-  (** val ggcd : positive -> positive -> positive * (positive * positive) **)
-  
-  let ggcd a b =
-    ggcdn (plus (size_nat a) (size_nat b)) a b
-  
-  (** val coq_Nsucc_double : n -> n **)
-  
-  let coq_Nsucc_double = function
-  | N0 -> Npos XH
-  | Npos p -> Npos (XI p)
-  
-  (** val coq_Ndouble : n -> n **)
-  
-  let coq_Ndouble = function
-  | N0 -> N0
-  | Npos p -> Npos (XO p)
-  
-  (** val coq_lor : positive -> positive -> positive **)
-  
-  let rec coq_lor p q0 =
-    match p with
-    | XI p2 ->
-      (match q0 with
-       | XI q1 -> XI (coq_lor p2 q1)
-       | XO q1 -> XI (coq_lor p2 q1)
-       | XH -> p)
-    | XO p2 ->
-      (match q0 with
-       | XI q1 -> XI (coq_lor p2 q1)
-       | XO q1 -> XO (coq_lor p2 q1)
-       | XH -> XI p2)
-    | XH ->
-      (match q0 with
-       | XO q1 -> XI q1
-       | _ -> q0)
-  
-  (** val coq_land : positive -> positive -> n **)
-  
-  let rec coq_land p q0 =
-    match p with
-    | XI p2 ->
-      (match q0 with
-       | XI q1 -> coq_Nsucc_double (coq_land p2 q1)
-       | XO q1 -> coq_Ndouble (coq_land p2 q1)
-       | XH -> Npos XH)
-    | XO p2 ->
-      (match q0 with
-       | XI q1 -> coq_Ndouble (coq_land p2 q1)
-       | XO q1 -> coq_Ndouble (coq_land p2 q1)
-       | XH -> N0)
-    | XH ->
-      (match q0 with
-       | XO q1 -> N0
-       | _ -> Npos XH)
-  
-  (** val ldiff : positive -> positive -> n **)
-  
-  let rec ldiff p q0 =
-    match p with
-    | XI p2 ->
-      (match q0 with
-       | XI q1 -> coq_Ndouble (ldiff p2 q1)
-       | XO q1 -> coq_Nsucc_double (ldiff p2 q1)
-       | XH -> Npos (XO p2))
-    | XO p2 ->
-      (match q0 with
-       | XI q1 -> coq_Ndouble (ldiff p2 q1)
-       | XO q1 -> coq_Ndouble (ldiff p2 q1)
-       | XH -> Npos p)
-    | XH ->
-      (match q0 with
-       | XO q1 -> Npos XH
-       | _ -> N0)
-  
-  (** val coq_lxor : positive -> positive -> n **)
-  
-  let rec coq_lxor p q0 =
-    match p with
-    | XI p2 ->
-      (match q0 with
-       | XI q1 -> coq_Ndouble (coq_lxor p2 q1)
-       | XO q1 -> coq_Nsucc_double (coq_lxor p2 q1)
-       | XH -> Npos (XO p2))
-    | XO p2 ->
-      (match q0 with
-       | XI q1 -> coq_Nsucc_double (coq_lxor p2 q1)
-       | XO q1 -> coq_Ndouble (coq_lxor p2 q1)
-       | XH -> Npos (XI p2))
-    | XH ->
-      (match q0 with
-       | XI q1 -> Npos (XO q1)
-       | XO q1 -> Npos (XI q1)
-       | XH -> N0)
-  
-  (** val shiftl_nat : positive -> nat -> positive **)
-  
-  let shiftl_nat p n0 =
-    nat_iter n0 (fun x -> XO x) p
-  
-  (** val shiftr_nat : positive -> nat -> positive **)
-  
-  let shiftr_nat p n0 =
-    nat_iter n0 div2 p
-  
-  (** val shiftl : positive -> n -> positive **)
-  
-  let shiftl p = function
-  | N0 -> p
-  | Npos n1 -> iter n1 (fun x -> XO x) p
-  
-  (** val shiftr : positive -> n -> positive **)
-  
-  let shiftr p = function
-  | N0 -> p
-  | Npos n1 -> iter n1 div2 p
-  
-  (** val testbit_nat : positive -> nat -> bool **)
-  
-  let rec testbit_nat p n0 =
-    match p with
-    | XI p2 ->
-      (match n0 with
-       | O -> true
-       | S n' -> testbit_nat p2 n')
-    | XO p2 ->
-      (match n0 with
-       | O -> false
-       | S n' -> testbit_nat p2 n')
-    | XH ->
-      (match n0 with
-       | O -> true
-       | S n1 -> false)
-  
-  (** val testbit : positive -> n -> bool **)
-  
-  let rec testbit p n0 =
-    match p with
-    | XI p2 ->
-      (match n0 with
-       | N0 -> true
-       | Npos n1 -> testbit p2 (pred_N n1))
-    | XO p2 ->
-      (match n0 with
-       | N0 -> false
-       | Npos n1 -> testbit p2 (pred_N n1))
-    | XH ->
-      (match n0 with
-       | N0 -> true
-       | Npos p2 -> false)
-  
-  (** val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 **)
-  
-  let rec iter_op op p a =
-    match p with
-    | XI p2 -> op a (iter_op op p2 (op a a))
-    | XO p2 -> iter_op op p2 (op a a)
-    | XH -> a
-  
-  (** val to_nat : positive -> nat **)
-  
-  let to_nat x =
-    iter_op plus x (S O)
-  
-  (** val of_nat : nat -> positive **)
-  
-  let rec of_nat = function
-  | O -> XH
-  | S x ->
-    (match x with
-     | O -> XH
-     | S n1 -> succ (of_nat x))
-  
-  (** val of_succ_nat : nat -> positive **)
-  
-  let rec of_succ_nat = function
-  | O -> XH
-  | S x -> succ (of_succ_nat x)
  end
 
-module Coq_Pos = 
- struct 
-  module Coq__1 = struct 
-   type t = positive
-  end
-  type t = Coq__1.t
-  
+module Coq_Pos =
+ struct
   (** val succ : positive -> positive **)
-  
+
   let rec succ = function
   | XI p -> XO (succ p)
   | XO p -> XI p
   | XH -> XO XH
-  
+
   (** val add : positive -> positive -> positive **)
-  
+
   let rec add x y =
     match x with
     | XI p ->
@@ -694,9 +87,9 @@ module Coq_Pos =
        | XI q0 -> XO (succ q0)
        | XO q0 -> XI q0
        | XH -> XO XH)
-  
+
   (** val add_carry : positive -> positive -> positive **)
-  
+
   and add_carry x y =
     match x with
     | XI p ->
@@ -714,78 +107,41 @@ module Coq_Pos =
        | XI q0 -> XI (succ q0)
        | XO q0 -> XO (succ q0)
        | XH -> XI XH)
-  
+
   (** val pred_double : positive -> positive **)
-  
+
   let rec pred_double = function
   | XI p -> XI (XO p)
   | XO p -> XI (pred_double p)
   | XH -> XH
-  
-  (** val pred : positive -> positive **)
-  
-  let pred = function
-  | XI p -> XO p
-  | XO p -> pred_double p
-  | XH -> XH
-  
-  (** val pred_N : positive -> n **)
-  
-  let pred_N = function
-  | XI p -> Npos (XO p)
-  | XO p -> Npos (pred_double p)
-  | XH -> N0
-  
+
   type mask = Pos.mask =
   | IsNul
   | IsPos of positive
   | IsNeg
-  
-  (** val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 **)
-  
-  let mask_rect f f0 f1 = function
-  | IsNul -> f
-  | IsPos x -> f0 x
-  | IsNeg -> f1
-  
-  (** val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 **)
-  
-  let mask_rec f f0 f1 = function
-  | IsNul -> f
-  | IsPos x -> f0 x
-  | IsNeg -> f1
-  
+
   (** val succ_double_mask : mask -> mask **)
-  
+
   let succ_double_mask = function
   | IsNul -> IsPos XH
   | IsPos p -> IsPos (XI p)
   | IsNeg -> IsNeg
-  
+
   (** val double_mask : mask -> mask **)
-  
+
   let double_mask = function
   | IsPos p -> IsPos (XO p)
   | x0 -> x0
-  
+
   (** val double_pred_mask : positive -> mask **)
-  
+
   let double_pred_mask = function
   | XI p -> IsPos (XO (XO p))
   | XO p -> IsPos (XO (pred_double p))
   | XH -> IsNul
-  
-  (** val pred_mask : mask -> mask **)
-  
-  let pred_mask = function
-  | IsPos q0 ->
-    (match q0 with
-     | XH -> IsNul
-     | _ -> IsPos (pred q0))
-  | _ -> IsNeg
-  
+
   (** val sub_mask : positive -> positive -> mask **)
-  
+
   let rec sub_mask x y =
     match x with
     | XI p ->
@@ -802,9 +158,9 @@ module Coq_Pos =
       (match y with
        | XH -> IsNul
        | _ -> IsNeg)
-  
+
   (** val sub_mask_carry : positive -> positive -> mask **)
-  
+
   and sub_mask_carry x y =
     match x with
     | XI p ->
@@ -818,167 +174,56 @@ module Coq_Pos =
        | XO q0 -> succ_double_mask (sub_mask_carry p q0)
        | XH -> double_pred_mask p)
     | XH -> IsNeg
-  
+
   (** val sub : positive -> positive -> positive **)
-  
+
   let sub x y =
     match sub_mask x y with
     | IsPos z0 -> z0
     | _ -> XH
-  
+
   (** val mul : positive -> positive -> positive **)
-  
+
   let rec mul x y =
     match x with
     | XI p -> add y (XO (mul p y))
     | XO p -> XO (mul p y)
     | XH -> y
-  
-  (** val iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
-  
-  let rec iter n0 f x =
-    match n0 with
-    | XI n' -> f (iter n' f (iter n' f x))
-    | XO n' -> iter n' f (iter n' f x)
-    | XH -> f x
-  
-  (** val pow : positive -> positive -> positive **)
-  
-  let pow x y =
-    iter y (mul x) XH
-  
-  (** val div2 : positive -> positive **)
-  
-  let div2 = function
-  | XI p2 -> p2
-  | XO p2 -> p2
-  | XH -> XH
-  
-  (** val div2_up : positive -> positive **)
-  
-  let div2_up = function
-  | XI p2 -> succ p2
-  | XO p2 -> p2
-  | XH -> XH
-  
+
   (** val size_nat : positive -> nat **)
-  
+
   let rec size_nat = function
   | XI p2 -> S (size_nat p2)
   | XO p2 -> S (size_nat p2)
   | XH -> S O
-  
-  (** val size : positive -> positive **)
-  
-  let rec size = function
-  | XI p2 -> succ (size p2)
-  | XO p2 -> succ (size p2)
-  | XH -> XH
-  
-  (** val compare_cont : positive -> positive -> comparison -> comparison **)
-  
-  let rec compare_cont x y r =
+
+  (** val compare_cont :
+      comparison -> positive -> positive -> comparison **)
+
+  let rec compare_cont r x y =
     match x with
     | XI p ->
       (match y with
-       | XI q0 -> compare_cont p q0 r
-       | XO q0 -> compare_cont p q0 Gt
+       | XI q0 -> compare_cont r p q0
+       | XO q0 -> compare_cont Gt p q0
        | XH -> Gt)
     | XO p ->
       (match y with
-       | XI q0 -> compare_cont p q0 Lt
-       | XO q0 -> compare_cont p q0 r
+       | XI q0 -> compare_cont Lt p q0
+       | XO q0 -> compare_cont r p q0
        | XH -> Gt)
     | XH ->
       (match y with
        | XH -> r
        | _ -> Lt)
-  
+
   (** val compare : positive -> positive -> comparison **)
-  
-  let compare x y =
-    compare_cont x y Eq
-  
-  (** val min : positive -> positive -> positive **)
-  
-  let min p p' =
-    match compare p p' with
-    | Gt -> p'
-    | _ -> p
-  
-  (** val max : positive -> positive -> positive **)
-  
-  let max p p' =
-    match compare p p' with
-    | Gt -> p
-    | _ -> p'
-  
-  (** val eqb : positive -> positive -> bool **)
-  
-  let rec eqb p q0 =
-    match p with
-    | XI p2 ->
-      (match q0 with
-       | XI q1 -> eqb p2 q1
-       | _ -> false)
-    | XO p2 ->
-      (match q0 with
-       | XO q1 -> eqb p2 q1
-       | _ -> false)
-    | XH ->
-      (match q0 with
-       | XH -> true
-       | _ -> false)
-  
-  (** val leb : positive -> positive -> bool **)
-  
-  let leb x y =
-    match compare x y with
-    | Gt -> false
-    | _ -> true
-  
-  (** val ltb : positive -> positive -> bool **)
-  
-  let ltb x y =
-    match compare x y with
-    | Lt -> true
-    | _ -> false
-  
-  (** val sqrtrem_step :
-      (positive -> positive) -> (positive -> positive) -> (positive * mask)
-      -> positive * mask **)
-  
-  let sqrtrem_step f g = function
-  | s,y ->
-    (match y with
-     | IsPos r ->
-       let s' = XI (XO s) in
-       let r' = g (f r) in
-       if leb s' r' then (XI s),(sub_mask r' s') else (XO s),(IsPos r')
-     | _ -> (XO s),(sub_mask (g (f XH)) (XO (XO XH))))
-  
-  (** val sqrtrem : positive -> positive * mask **)
-  
-  let rec sqrtrem = function
-  | XI p2 ->
-    (match p2 with
-     | XI p3 -> sqrtrem_step (fun x -> XI x) (fun x -> XI x) (sqrtrem p3)
-     | XO p3 -> sqrtrem_step (fun x -> XO x) (fun x -> XI x) (sqrtrem p3)
-     | XH -> XH,(IsPos (XO XH)))
-  | XO p2 ->
-    (match p2 with
-     | XI p3 -> sqrtrem_step (fun x -> XI x) (fun x -> XO x) (sqrtrem p3)
-     | XO p3 -> sqrtrem_step (fun x -> XO x) (fun x -> XO x) (sqrtrem p3)
-     | XH -> XH,(IsPos XH))
-  | XH -> XH,IsNul
-  
-  (** val sqrt : positive -> positive **)
-  
-  let sqrt p =
-    fst (sqrtrem p)
-  
+
+  let compare =
+    compare_cont Eq
+
   (** val gcdn : nat -> positive -> positive -> positive **)
-  
+
   let rec gcdn n0 a b =
     match n0 with
     | O -> XH
@@ -995,1001 +240,30 @@ module Coq_Pos =
           | XH -> XH)
        | XO a0 ->
          (match b with
-          | XI p -> gcdn n1 a0 b
+          | XI _ -> gcdn n1 a0 b
           | XO b0 -> XO (gcdn n1 a0 b0)
           | XH -> XH)
        | XH -> XH)
-  
+
   (** val gcd : positive -> positive -> positive **)
-  
+
   let gcd a b =
-    gcdn (plus (size_nat a) (size_nat b)) a b
-  
-  (** val ggcdn :
-      nat -> positive -> positive -> positive * (positive * positive) **)
-  
-  let rec ggcdn n0 a b =
-    match n0 with
-    | O -> XH,(a,b)
-    | S n1 ->
-      (match a with
-       | XI a' ->
-         (match b with
-          | XI b' ->
-            (match compare a' b' with
-             | Eq -> a,(XH,XH)
-             | Lt ->
-               let g,p = ggcdn n1 (sub b' a') a in
-               let ba,aa = p in g,(aa,(add aa (XO ba)))
-             | Gt ->
-               let g,p = ggcdn n1 (sub a' b') b in
-               let ab,bb = p in g,((add bb (XO ab)),bb))
-          | XO b0 ->
-            let g,p = ggcdn n1 a b0 in let aa,bb = p in g,(aa,(XO bb))
-          | XH -> XH,(a,XH))
-       | XO a0 ->
-         (match b with
-          | XI p ->
-            let g,p2 = ggcdn n1 a0 b in let aa,bb = p2 in g,((XO aa),bb)
-          | XO b0 -> let g,p = ggcdn n1 a0 b0 in (XO g),p
-          | XH -> XH,(a,XH))
-       | XH -> XH,(XH,b))
-  
-  (** val ggcd : positive -> positive -> positive * (positive * positive) **)
-  
-  let ggcd a b =
-    ggcdn (plus (size_nat a) (size_nat b)) a b
-  
-  (** val coq_Nsucc_double : n -> n **)
-  
-  let coq_Nsucc_double = function
-  | N0 -> Npos XH
-  | Npos p -> Npos (XI p)
-  
-  (** val coq_Ndouble : n -> n **)
-  
-  let coq_Ndouble = function
-  | N0 -> N0
-  | Npos p -> Npos (XO p)
-  
-  (** val coq_lor : positive -> positive -> positive **)
-  
-  let rec coq_lor p q0 =
-    match p with
-    | XI p2 ->
-      (match q0 with
-       | XI q1 -> XI (coq_lor p2 q1)
-       | XO q1 -> XI (coq_lor p2 q1)
-       | XH -> p)
-    | XO p2 ->
-      (match q0 with
-       | XI q1 -> XI (coq_lor p2 q1)
-       | XO q1 -> XO (coq_lor p2 q1)
-       | XH -> XI p2)
-    | XH ->
-      (match q0 with
-       | XO q1 -> XI q1
-       | _ -> q0)
-  
-  (** val coq_land : positive -> positive -> n **)
-  
-  let rec coq_land p q0 =
-    match p with
-    | XI p2 ->
-      (match q0 with
-       | XI q1 -> coq_Nsucc_double (coq_land p2 q1)
-       | XO q1 -> coq_Ndouble (coq_land p2 q1)
-       | XH -> Npos XH)
-    | XO p2 ->
-      (match q0 with
-       | XI q1 -> coq_Ndouble (coq_land p2 q1)
-       | XO q1 -> coq_Ndouble (coq_land p2 q1)
-       | XH -> N0)
-    | XH ->
-      (match q0 with
-       | XO q1 -> N0
-       | _ -> Npos XH)
-  
-  (** val ldiff : positive -> positive -> n **)
-  
-  let rec ldiff p q0 =
-    match p with
-    | XI p2 ->
-      (match q0 with
-       | XI q1 -> coq_Ndouble (ldiff p2 q1)
-       | XO q1 -> coq_Nsucc_double (ldiff p2 q1)
-       | XH -> Npos (XO p2))
-    | XO p2 ->
-      (match q0 with
-       | XI q1 -> coq_Ndouble (ldiff p2 q1)
-       | XO q1 -> coq_Ndouble (ldiff p2 q1)
-       | XH -> Npos p)
-    | XH ->
-      (match q0 with
-       | XO q1 -> Npos XH
-       | _ -> N0)
-  
-  (** val coq_lxor : positive -> positive -> n **)
-  
-  let rec coq_lxor p q0 =
-    match p with
-    | XI p2 ->
-      (match q0 with
-       | XI q1 -> coq_Ndouble (coq_lxor p2 q1)
-       | XO q1 -> coq_Nsucc_double (coq_lxor p2 q1)
-       | XH -> Npos (XO p2))
-    | XO p2 ->
-      (match q0 with
-       | XI q1 -> coq_Nsucc_double (coq_lxor p2 q1)
-       | XO q1 -> coq_Ndouble (coq_lxor p2 q1)
-       | XH -> Npos (XI p2))
-    | XH ->
-      (match q0 with
-       | XI q1 -> Npos (XO q1)
-       | XO q1 -> Npos (XI q1)
-       | XH -> N0)
-  
-  (** val shiftl_nat : positive -> nat -> positive **)
-  
-  let shiftl_nat p n0 =
-    nat_iter n0 (fun x -> XO x) p
-  
-  (** val shiftr_nat : positive -> nat -> positive **)
-  
-  let shiftr_nat p n0 =
-    nat_iter n0 div2 p
-  
-  (** val shiftl : positive -> n -> positive **)
-  
-  let shiftl p = function
-  | N0 -> p
-  | Npos n1 -> iter n1 (fun x -> XO x) p
-  
-  (** val shiftr : positive -> n -> positive **)
-  
-  let shiftr p = function
-  | N0 -> p
-  | Npos n1 -> iter n1 div2 p
-  
-  (** val testbit_nat : positive -> nat -> bool **)
-  
-  let rec testbit_nat p n0 =
-    match p with
-    | XI p2 ->
-      (match n0 with
-       | O -> true
-       | S n' -> testbit_nat p2 n')
-    | XO p2 ->
-      (match n0 with
-       | O -> false
-       | S n' -> testbit_nat p2 n')
-    | XH ->
-      (match n0 with
-       | O -> true
-       | S n1 -> false)
-  
-  (** val testbit : positive -> n -> bool **)
-  
-  let rec testbit p n0 =
-    match p with
-    | XI p2 ->
-      (match n0 with
-       | N0 -> true
-       | Npos n1 -> testbit p2 (pred_N n1))
-    | XO p2 ->
-      (match n0 with
-       | N0 -> false
-       | Npos n1 -> testbit p2 (pred_N n1))
-    | XH ->
-      (match n0 with
-       | N0 -> true
-       | Npos p2 -> false)
-  
-  (** val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 **)
-  
-  let rec iter_op op p a =
-    match p with
-    | XI p2 -> op a (iter_op op p2 (op a a))
-    | XO p2 -> iter_op op p2 (op a a)
-    | XH -> a
-  
-  (** val to_nat : positive -> nat **)
-  
-  let to_nat x =
-    iter_op plus x (S O)
-  
-  (** val of_nat : nat -> positive **)
-  
-  let rec of_nat = function
-  | O -> XH
-  | S x ->
-    (match x with
-     | O -> XH
-     | S n1 -> succ (of_nat x))
-  
+    gcdn (Coq__1.add (size_nat a) (size_nat b)) a b
+
   (** val of_succ_nat : nat -> positive **)
-  
+
   let rec of_succ_nat = function
   | O -> XH
   | S x -> succ (of_succ_nat x)
-  
-  (** val eq_dec : positive -> positive -> bool **)
-  
-  let rec eq_dec p y0 =
-    match p with
-    | XI p2 ->
-      (match y0 with
-       | XI p3 -> eq_dec p2 p3
-       | _ -> false)
-    | XO p2 ->
-      (match y0 with
-       | XO p3 -> eq_dec p2 p3
-       | _ -> false)
-    | XH ->
-      (match y0 with
-       | XH -> true
-       | _ -> false)
-  
-  (** val peano_rect : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1 **)
-  
-  let rec peano_rect a f p =
-    let f2 = peano_rect (f XH a) (fun p2 x -> f (succ (XO p2)) (f (XO p2) x))
-    in
-    (match p with
-     | XI q0 -> f (XO q0) (f2 q0)
-     | XO q0 -> f2 q0
-     | XH -> a)
-  
-  (** val peano_rec : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1 **)
-  
-  let peano_rec =
-    peano_rect
-  
-  type coq_PeanoView =
-  | PeanoOne
-  | PeanoSucc of positive * coq_PeanoView
-  
-  (** val coq_PeanoView_rect :
-      'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive ->
-      coq_PeanoView -> 'a1 **)
-  
-  let rec coq_PeanoView_rect f f0 p = function
-  | PeanoOne -> f
-  | PeanoSucc (p3, p4) -> f0 p3 p4 (coq_PeanoView_rect f f0 p3 p4)
-  
-  (** val coq_PeanoView_rec :
-      'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive ->
-      coq_PeanoView -> 'a1 **)
-  
-  let rec coq_PeanoView_rec f f0 p = function
-  | PeanoOne -> f
-  | PeanoSucc (p3, p4) -> f0 p3 p4 (coq_PeanoView_rec f f0 p3 p4)
-  
-  (** val peanoView_xO : positive -> coq_PeanoView -> coq_PeanoView **)
-  
-  let rec peanoView_xO p = function
-  | PeanoOne -> PeanoSucc (XH, PeanoOne)
-  | PeanoSucc (p2, q1) ->
-    PeanoSucc ((succ (XO p2)), (PeanoSucc ((XO p2), (peanoView_xO p2 q1))))
-  
-  (** val peanoView_xI : positive -> coq_PeanoView -> coq_PeanoView **)
-  
-  let rec peanoView_xI p = function
-  | PeanoOne -> PeanoSucc ((succ XH), (PeanoSucc (XH, PeanoOne)))
-  | PeanoSucc (p2, q1) ->
-    PeanoSucc ((succ (XI p2)), (PeanoSucc ((XI p2), (peanoView_xI p2 q1))))
-  
-  (** val peanoView : positive -> coq_PeanoView **)
-  
-  let rec peanoView = function
-  | XI p2 -> peanoView_xI p2 (peanoView p2)
-  | XO p2 -> peanoView_xO p2 (peanoView p2)
-  | XH -> PeanoOne
-  
-  (** val coq_PeanoView_iter :
-      'a1 -> (positive -> 'a1 -> 'a1) -> positive -> coq_PeanoView -> 'a1 **)
-  
-  let rec coq_PeanoView_iter a f p = function
-  | PeanoOne -> a
-  | PeanoSucc (p2, q1) -> f p2 (coq_PeanoView_iter a f p2 q1)
-  
-  (** val switch_Eq : comparison -> comparison -> comparison **)
-  
-  let switch_Eq c = function
-  | Eq -> c
-  | x -> x
-  
-  (** val mask2cmp : mask -> comparison **)
-  
-  let mask2cmp = function
-  | IsNul -> Eq
-  | IsPos p2 -> Gt
-  | IsNeg -> Lt
-  
-  module T = 
-   struct 
-    
-   end
-  
-  module ORev = 
-   struct 
-    type t = Coq__1.t
-   end
-  
-  module MRev = 
-   struct 
-    (** val max : t -> t -> t **)
-    
-    let max x y =
-      min y x
-   end
-  
-  module MPRev = MaxLogicalProperties(ORev)(MRev)
-  
-  module P = 
-   struct 
-    (** val max_case_strong :
-        t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-        -> 'a1 **)
-    
-    let max_case_strong n0 m compat hl hr =
-      let c = compSpec2Type n0 m (compare n0 m) in
-      (match c with
-       | CompGtT -> compat n0 (max n0 m) __ (hl __)
-       | _ -> compat m (max n0 m) __ (hr __))
-    
-    (** val max_case :
-        t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **)
-    
-    let max_case n0 m x x0 x1 =
-      max_case_strong n0 m x (fun _ -> x0) (fun _ -> x1)
-    
-    (** val max_dec : t -> t -> bool **)
-    
-    let max_dec n0 m =
-      max_case n0 m (fun x y _ h0 -> h0) true false
-    
-    (** val min_case_strong :
-        t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-        -> 'a1 **)
-    
-    let min_case_strong n0 m compat hl hr =
-      let c = compSpec2Type n0 m (compare n0 m) in
-      (match c with
-       | CompGtT -> compat m (min n0 m) __ (hr __)
-       | _ -> compat n0 (min n0 m) __ (hl __))
-    
-    (** val min_case :
-        t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **)
-    
-    let min_case n0 m x x0 x1 =
-      min_case_strong n0 m x (fun _ -> x0) (fun _ -> x1)
-    
-    (** val min_dec : t -> t -> bool **)
-    
-    let min_dec n0 m =
-      min_case n0 m (fun x y _ h0 -> h0) true false
-   end
-  
-  (** val max_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
-  
-  let max_case_strong n0 m x x0 =
-    P.max_case_strong n0 m (fun x1 y _ x2 -> x2) x x0
-  
-  (** val max_case : t -> t -> 'a1 -> 'a1 -> 'a1 **)
-  
-  let max_case n0 m x x0 =
-    max_case_strong n0 m (fun _ -> x) (fun _ -> x0)
-  
-  (** val max_dec : t -> t -> bool **)
-  
-  let max_dec =
-    P.max_dec
-  
-  (** val min_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
-  
-  let min_case_strong n0 m x x0 =
-    P.min_case_strong n0 m (fun x1 y _ x2 -> x2) x x0
-  
-  (** val min_case : t -> t -> 'a1 -> 'a1 -> 'a1 **)
-  
-  let min_case n0 m x x0 =
-    min_case_strong n0 m (fun _ -> x) (fun _ -> x0)
-  
-  (** val min_dec : t -> t -> bool **)
-  
-  let min_dec =
-    P.min_dec
  end
 
-module N = 
- struct 
-  type t = n
-  
-  (** val zero : n **)
-  
-  let zero =
-    N0
-  
-  (** val one : n **)
-  
-  let one =
-    Npos XH
-  
-  (** val two : n **)
-  
-  let two =
-    Npos (XO XH)
-  
-  (** val succ_double : n -> n **)
-  
-  let succ_double = function
-  | N0 -> Npos XH
-  | Npos p -> Npos (XI p)
-  
-  (** val double : n -> n **)
-  
-  let double = function
-  | N0 -> N0
-  | Npos p -> Npos (XO p)
-  
-  (** val succ : n -> n **)
-  
-  let succ = function
-  | N0 -> Npos XH
-  | Npos p -> Npos (Coq_Pos.succ p)
-  
-  (** val pred : n -> n **)
-  
-  let pred = function
-  | N0 -> N0
-  | Npos p -> Coq_Pos.pred_N p
-  
-  (** val succ_pos : n -> positive **)
-  
-  let succ_pos = function
-  | N0 -> XH
-  | Npos p -> Coq_Pos.succ p
-  
-  (** val add : n -> n -> n **)
-  
-  let add n0 m =
-    match n0 with
-    | N0 -> m
-    | Npos p ->
-      (match m with
-       | N0 -> n0
-       | Npos q0 -> Npos (Coq_Pos.add p q0))
-  
-  (** val sub : n -> n -> n **)
-  
-  let sub n0 m =
-    match n0 with
-    | N0 -> N0
-    | Npos n' ->
-      (match m with
-       | N0 -> n0
-       | Npos m' ->
-         (match Coq_Pos.sub_mask n' m' with
-          | Coq_Pos.IsPos p -> Npos p
-          | _ -> N0))
-  
-  (** val mul : n -> n -> n **)
-  
-  let mul n0 m =
-    match n0 with
-    | N0 -> N0
-    | Npos p ->
-      (match m with
-       | N0 -> N0
-       | Npos q0 -> Npos (Coq_Pos.mul p q0))
-  
-  (** val compare : n -> n -> comparison **)
-  
-  let compare n0 m =
-    match n0 with
-    | N0 ->
-      (match m with
-       | N0 -> Eq
-       | Npos m' -> Lt)
-    | Npos n' ->
-      (match m with
-       | N0 -> Gt
-       | Npos m' -> Coq_Pos.compare n' m')
-  
-  (** val eqb : n -> n -> bool **)
-  
-  let eqb n0 m =
-    match n0 with
-    | N0 ->
-      (match m with
-       | N0 -> true
-       | Npos p -> false)
-    | Npos p ->
-      (match m with
-       | N0 -> false
-       | Npos q0 -> Coq_Pos.eqb p q0)
-  
-  (** val leb : n -> n -> bool **)
-  
-  let leb x y =
-    match compare x y with
-    | Gt -> false
-    | _ -> true
-  
-  (** val ltb : n -> n -> bool **)
-  
-  let ltb x y =
-    match compare x y with
-    | Lt -> true
-    | _ -> false
-  
-  (** val min : n -> n -> n **)
-  
-  let min n0 n' =
-    match compare n0 n' with
-    | Gt -> n'
-    | _ -> n0
-  
-  (** val max : n -> n -> n **)
-  
-  let max n0 n' =
-    match compare n0 n' with
-    | Gt -> n0
-    | _ -> n'
-  
-  (** val div2 : n -> n **)
-  
-  let div2 = function
-  | N0 -> N0
-  | Npos p2 ->
-    (match p2 with
-     | XI p -> Npos p
-     | XO p -> Npos p
-     | XH -> N0)
-  
-  (** val even : n -> bool **)
-  
-  let even = function
-  | N0 -> true
-  | Npos p ->
-    (match p with
-     | XO p2 -> true
-     | _ -> false)
-  
-  (** val odd : n -> bool **)
-  
-  let odd n0 =
-    negb (even n0)
-  
-  (** val pow : n -> n -> n **)
-  
-  let pow n0 = function
-  | N0 -> Npos XH
-  | Npos p2 ->
-    (match n0 with
-     | N0 -> N0
-     | Npos q0 -> Npos (Coq_Pos.pow q0 p2))
-  
-  (** val log2 : n -> n **)
-  
-  let log2 = function
-  | N0 -> N0
-  | Npos p2 ->
-    (match p2 with
-     | XI p -> Npos (Coq_Pos.size p)
-     | XO p -> Npos (Coq_Pos.size p)
-     | XH -> N0)
-  
-  (** val size : n -> n **)
-  
-  let size = function
-  | N0 -> N0
-  | Npos p -> Npos (Coq_Pos.size p)
-  
-  (** val size_nat : n -> nat **)
-  
-  let size_nat = function
-  | N0 -> O
-  | Npos p -> Coq_Pos.size_nat p
-  
-  (** val pos_div_eucl : positive -> n -> n * n **)
-  
-  let rec pos_div_eucl a b =
-    match a with
-    | XI a' ->
-      let q0,r = pos_div_eucl a' b in
-      let r' = succ_double r in
-      if leb b r' then (succ_double q0),(sub r' b) else (double q0),r'
-    | XO a' ->
-      let q0,r = pos_div_eucl a' b in
-      let r' = double r in
-      if leb b r' then (succ_double q0),(sub r' b) else (double q0),r'
-    | XH ->
-      (match b with
-       | N0 -> N0,(Npos XH)
-       | Npos p ->
-         (match p with
-          | XH -> (Npos XH),N0
-          | _ -> N0,(Npos XH)))
-  
-  (** val div_eucl : n -> n -> n * n **)
-  
-  let div_eucl a b =
-    match a with
-    | N0 -> N0,N0
-    | Npos na ->
-      (match b with
-       | N0 -> N0,a
-       | Npos p -> pos_div_eucl na b)
-  
-  (** val div : n -> n -> n **)
-  
-  let div a b =
-    fst (div_eucl a b)
-  
-  (** val modulo : n -> n -> n **)
-  
-  let modulo a b =
-    snd (div_eucl a b)
-  
-  (** val gcd : n -> n -> n **)
-  
-  let gcd a b =
-    match a with
-    | N0 -> b
-    | Npos p ->
-      (match b with
-       | N0 -> a
-       | Npos q0 -> Npos (Coq_Pos.gcd p q0))
-  
-  (** val ggcd : n -> n -> n * (n * n) **)
-  
-  let ggcd a b =
-    match a with
-    | N0 -> b,(N0,(Npos XH))
-    | Npos p ->
-      (match b with
-       | N0 -> a,((Npos XH),N0)
-       | Npos q0 ->
-         let g,p2 = Coq_Pos.ggcd p q0 in
-         let aa,bb = p2 in (Npos g),((Npos aa),(Npos bb)))
-  
-  (** val sqrtrem : n -> n * n **)
-  
-  let sqrtrem = function
-  | N0 -> N0,N0
-  | Npos p ->
-    let s,m = Coq_Pos.sqrtrem p in
-    (match m with
-     | Coq_Pos.IsPos r -> (Npos s),(Npos r)
-     | _ -> (Npos s),N0)
-  
-  (** val sqrt : n -> n **)
-  
-  let sqrt = function
-  | N0 -> N0
-  | Npos p -> Npos (Coq_Pos.sqrt p)
-  
-  (** val coq_lor : n -> n -> n **)
-  
-  let coq_lor n0 m =
-    match n0 with
-    | N0 -> m
-    | Npos p ->
-      (match m with
-       | N0 -> n0
-       | Npos q0 -> Npos (Coq_Pos.coq_lor p q0))
-  
-  (** val coq_land : n -> n -> n **)
-  
-  let coq_land n0 m =
-    match n0 with
-    | N0 -> N0
-    | Npos p ->
-      (match m with
-       | N0 -> N0
-       | Npos q0 -> Coq_Pos.coq_land p q0)
-  
-  (** val ldiff : n -> n -> n **)
-  
-  let ldiff n0 m =
-    match n0 with
-    | N0 -> N0
-    | Npos p ->
-      (match m with
-       | N0 -> n0
-       | Npos q0 -> Coq_Pos.ldiff p q0)
-  
-  (** val coq_lxor : n -> n -> n **)
-  
-  let coq_lxor n0 m =
-    match n0 with
-    | N0 -> m
-    | Npos p ->
-      (match m with
-       | N0 -> n0
-       | Npos q0 -> Coq_Pos.coq_lxor p q0)
-  
-  (** val shiftl_nat : n -> nat -> n **)
-  
-  let shiftl_nat a n0 =
-    nat_iter n0 double a
-  
-  (** val shiftr_nat : n -> nat -> n **)
-  
-  let shiftr_nat a n0 =
-    nat_iter n0 div2 a
-  
-  (** val shiftl : n -> n -> n **)
-  
-  let shiftl a n0 =
-    match a with
-    | N0 -> N0
-    | Npos a0 -> Npos (Coq_Pos.shiftl a0 n0)
-  
-  (** val shiftr : n -> n -> n **)
-  
-  let shiftr a = function
-  | N0 -> a
-  | Npos p -> Coq_Pos.iter p div2 a
-  
-  (** val testbit_nat : n -> nat -> bool **)
-  
-  let testbit_nat = function
-  | N0 -> (fun x -> false)
-  | Npos p -> Coq_Pos.testbit_nat p
-  
-  (** val testbit : n -> n -> bool **)
-  
-  let testbit a n0 =
-    match a with
-    | N0 -> false
-    | Npos p -> Coq_Pos.testbit p n0
-  
-  (** val to_nat : n -> nat **)
-  
-  let to_nat = function
-  | N0 -> O
-  | Npos p -> Coq_Pos.to_nat p
-  
+module N =
+ struct
   (** val of_nat : nat -> n **)
-  
+
   let of_nat = function
   | O -> N0
   | S n' -> Npos (Coq_Pos.of_succ_nat n')
-  
-  (** val iter : n -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
-  
-  let iter n0 f x =
-    match n0 with
-    | N0 -> x
-    | Npos p -> Coq_Pos.iter p f x
-  
-  (** val eq_dec : n -> n -> bool **)
-  
-  let eq_dec n0 m =
-    match n0 with
-    | N0 ->
-      (match m with
-       | N0 -> true
-       | Npos p -> false)
-    | Npos x ->
-      (match m with
-       | N0 -> false
-       | Npos p2 -> Coq_Pos.eq_dec x p2)
-  
-  (** val discr : n -> positive option **)
-  
-  let discr = function
-  | N0 -> None
-  | Npos p -> Some p
-  
-  (** val binary_rect :
-      'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1 **)
-  
-  let binary_rect f0 f2 fS2 n0 =
-    let f2' = fun p -> f2 (Npos p) in
-    let fS2' = fun p -> fS2 (Npos p) in
-    (match n0 with
-     | N0 -> f0
-     | Npos p ->
-       let rec f = function
-       | XI p3 -> fS2' p3 (f p3)
-       | XO p3 -> f2' p3 (f p3)
-       | XH -> fS2 N0 f0
-       in f p)
-  
-  (** val binary_rec :
-      'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1 **)
-  
-  let binary_rec =
-    binary_rect
-  
-  (** val peano_rect : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 **)
-  
-  let peano_rect f0 f n0 =
-    let f' = fun p -> f (Npos p) in
-    (match n0 with
-     | N0 -> f0
-     | Npos p -> Coq_Pos.peano_rect (f N0 f0) f' p)
-  
-  (** val peano_rec : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 **)
-  
-  let peano_rec =
-    peano_rect
-  
-  module BootStrap = 
-   struct 
-    
-   end
-  
-  (** val recursion : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 **)
-  
-  let recursion x =
-    peano_rect x
-  
-  module OrderElts = 
-   struct 
-    type t = n
-   end
-  
-  module OrderTac = MakeOrderTac(OrderElts)
-  
-  module NZPowP = 
-   struct 
-    
-   end
-  
-  module NZSqrtP = 
-   struct 
-    
-   end
-  
-  (** val sqrt_up : n -> n **)
-  
-  let sqrt_up a =
-    match compare N0 a with
-    | Lt -> succ (sqrt (pred a))
-    | _ -> N0
-  
-  (** val log2_up : n -> n **)
-  
-  let log2_up a =
-    match compare (Npos XH) a with
-    | Lt -> succ (log2 (pred a))
-    | _ -> N0
-  
-  module NZDivP = 
-   struct 
-    
-   end
-  
-  (** val lcm : n -> n -> n **)
-  
-  let lcm a b =
-    mul a (div b (gcd a b))
-  
-  (** val b2n : bool -> n **)
-  
-  let b2n = function
-  | true -> Npos XH
-  | false -> N0
-  
-  (** val setbit : n -> n -> n **)
-  
-  let setbit a n0 =
-    coq_lor a (shiftl (Npos XH) n0)
-  
-  (** val clearbit : n -> n -> n **)
-  
-  let clearbit a n0 =
-    ldiff a (shiftl (Npos XH) n0)
-  
-  (** val ones : n -> n **)
-  
-  let ones n0 =
-    pred (shiftl (Npos XH) n0)
-  
-  (** val lnot : n -> n -> n **)
-  
-  let lnot a n0 =
-    coq_lxor a (ones n0)
-  
-  module T = 
-   struct 
-    
-   end
-  
-  module ORev = 
-   struct 
-    type t = n
-   end
-  
-  module MRev = 
-   struct 
-    (** val max : n -> n -> n **)
-    
-    let max x y =
-      min y x
-   end
-  
-  module MPRev = MaxLogicalProperties(ORev)(MRev)
-  
-  module P = 
-   struct 
-    (** val max_case_strong :
-        n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-        -> 'a1 **)
-    
-    let max_case_strong n0 m compat hl hr =
-      let c = compSpec2Type n0 m (compare n0 m) in
-      (match c with
-       | CompGtT -> compat n0 (max n0 m) __ (hl __)
-       | _ -> compat m (max n0 m) __ (hr __))
-    
-    (** val max_case :
-        n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **)
-    
-    let max_case n0 m x x0 x1 =
-      max_case_strong n0 m x (fun _ -> x0) (fun _ -> x1)
-    
-    (** val max_dec : n -> n -> bool **)
-    
-    let max_dec n0 m =
-      max_case n0 m (fun x y _ h0 -> h0) true false
-    
-    (** val min_case_strong :
-        n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-        -> 'a1 **)
-    
-    let min_case_strong n0 m compat hl hr =
-      let c = compSpec2Type n0 m (compare n0 m) in
-      (match c with
-       | CompGtT -> compat m (min n0 m) __ (hr __)
-       | _ -> compat n0 (min n0 m) __ (hl __))
-    
-    (** val min_case :
-        n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **)
-    
-    let min_case n0 m x x0 x1 =
-      min_case_strong n0 m x (fun _ -> x0) (fun _ -> x1)
-    
-    (** val min_dec : n -> n -> bool **)
-    
-    let min_dec n0 m =
-      min_case n0 m (fun x y _ h0 -> h0) true false
-   end
-  
-  (** val max_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
-  
-  let max_case_strong n0 m x x0 =
-    P.max_case_strong n0 m (fun x1 y _ x2 -> x2) x x0
-  
-  (** val max_case : n -> n -> 'a1 -> 'a1 -> 'a1 **)
-  
-  let max_case n0 m x x0 =
-    max_case_strong n0 m (fun _ -> x) (fun _ -> x0)
-  
-  (** val max_dec : n -> n -> bool **)
-  
-  let max_dec =
-    P.max_dec
-  
-  (** val min_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
-  
-  let min_case_strong n0 m x x0 =
-    P.min_case_strong n0 m (fun x1 y _ x2 -> x2) x x0
-  
-  (** val min_case : n -> n -> 'a1 -> 'a1 -> 'a1 **)
-  
-  let min_case n0 m x x0 =
-    min_case_strong n0 m (fun _ -> x) (fun _ -> x0)
-  
-  (** val min_dec : n -> n -> bool **)
-  
-  let min_dec =
-    P.min_dec
  end
 
 (** val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 **)
@@ -2006,66 +280,49 @@ let rec nth n0 l default =
   | O ->
     (match l with
      | [] -> default
-     | x::l' -> x)
+     | x::_ -> x)
   | S m ->
     (match l with
      | [] -> default
-     | x::t1 -> nth m t1 default)
+     | _::t0 -> nth m t0 default)
 
 (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
 
 let rec map f = function
 | [] -> []
-| a::t1 -> (f a)::(map f t1)
+| a::t0 -> (f a)::(map f t0)
 
 (** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **)
 
 let rec fold_right f a0 = function
 | [] -> a0
-| b::t1 -> f b (fold_right f a0 t1)
-
-module Z = 
- struct 
-  type t = z
-  
-  (** val zero : z **)
-  
-  let zero =
-    Z0
-  
-  (** val one : z **)
-  
-  let one =
-    Zpos XH
-  
-  (** val two : z **)
-  
-  let two =
-    Zpos (XO XH)
-  
+| b::t0 -> f b (fold_right f a0 t0)
+
+module Z =
+ struct
   (** val double : z -> z **)
-  
+
   let double = function
   | Z0 -> Z0
   | Zpos p -> Zpos (XO p)
   | Zneg p -> Zneg (XO p)
-  
+
   (** val succ_double : z -> z **)
-  
+
   let succ_double = function
   | Z0 -> Zpos XH
   | Zpos p -> Zpos (XI p)
   | Zneg p -> Zneg (Coq_Pos.pred_double p)
-  
+
   (** val pred_double : z -> z **)
-  
+
   let pred_double = function
   | Z0 -> Zneg XH
   | Zpos p -> Zpos (Coq_Pos.pred_double p)
   | Zneg p -> Zneg (XI p)
-  
+
   (** val pos_sub : positive -> positive -> z **)
-  
+
   let rec pos_sub x y =
     match x with
     | XI p ->
@@ -2083,9 +340,9 @@ module Z =
        | XI q0 -> Zneg (XO q0)
        | XO q0 -> Zneg (Coq_Pos.pred_double q0)
        | XH -> Z0)
-  
+
   (** val add : z -> z -> z **)
-  
+
   let add x y =
     match x with
     | Z0 -> y
@@ -2099,31 +356,21 @@ module Z =
        | Z0 -> x
        | Zpos y' -> pos_sub y' x'
        | Zneg y' -> Zneg (Coq_Pos.add x' y'))
-  
+
   (** val opp : z -> z **)
-  
+
   let opp = function
   | Z0 -> Z0
   | Zpos x0 -> Zneg x0
   | Zneg x0 -> Zpos x0
-  
-  (** val succ : z -> z **)
-  
-  let succ x =
-    add x (Zpos XH)
-  
-  (** val pred : z -> z **)
-  
-  let pred x =
-    add x (Zneg XH)
-  
+
   (** val sub : z -> z -> z **)
-  
+
   let sub m n0 =
     add m (opp n0)
-  
+
   (** val mul : z -> z -> z **)
-  
+
   let mul x y =
     match x with
     | Z0 -> Z0
@@ -2137,28 +384,16 @@ module Z =
        | Z0 -> Z0
        | Zpos y' -> Zneg (Coq_Pos.mul x' y')
        | Zneg y' -> Zpos (Coq_Pos.mul x' y'))
-  
-  (** val pow_pos : z -> positive -> z **)
-  
-  let pow_pos z0 n0 =
-    Coq_Pos.iter n0 (mul z0) (Zpos XH)
-  
-  (** val pow : z -> z -> z **)
-  
-  let pow x = function
-  | Z0 -> Zpos XH
-  | Zpos p -> pow_pos x p
-  | Zneg p -> Z0
-  
+
   (** val compare : z -> z -> comparison **)
-  
+
   let compare x y =
     match x with
     | Z0 ->
       (match y with
        | Z0 -> Eq
-       | Zpos y' -> Lt
-       | Zneg y' -> Gt)
+       | Zpos _ -> Lt
+       | Zneg _ -> Gt)
     | Zpos x' ->
       (match y with
        | Zpos y' -> Coq_Pos.compare x' y'
@@ -2167,151 +402,74 @@ module Z =
       (match y with
        | Zneg y' -> compOpp (Coq_Pos.compare x' y')
        | _ -> Lt)
-  
-  (** val sgn : z -> z **)
-  
-  let sgn = function
-  | Z0 -> Z0
-  | Zpos p -> Zpos XH
-  | Zneg p -> Zneg XH
-  
+
   (** val leb : z -> z -> bool **)
-  
+
   let leb x y =
     match compare x y with
     | Gt -> false
     | _ -> true
-  
-  (** val geb : z -> z -> bool **)
-  
-  let geb x y =
-    match compare x y with
-    | Lt -> false
-    | _ -> true
-  
+
   (** val ltb : z -> z -> bool **)
-  
+
   let ltb x y =
     match compare x y with
     | Lt -> true
     | _ -> false
-  
+
   (** val gtb : z -> z -> bool **)
-  
+
   let gtb x y =
     match compare x y with
     | Gt -> true
     | _ -> false
-  
-  (** val eqb : z -> z -> bool **)
-  
-  let eqb x y =
-    match x with
-    | Z0 ->
-      (match y with
-       | Z0 -> true
-       | _ -> false)
-    | Zpos p ->
-      (match y with
-       | Zpos q0 -> Coq_Pos.eqb p q0
-       | _ -> false)
-    | Zneg p ->
-      (match y with
-       | Zneg q0 -> Coq_Pos.eqb p q0
-       | _ -> false)
-  
+
   (** val max : z -> z -> z **)
-  
+
   let max n0 m =
     match compare n0 m with
     | Lt -> m
     | _ -> n0
-  
-  (** val min : z -> z -> z **)
-  
-  let min n0 m =
-    match compare n0 m with
-    | Gt -> m
-    | _ -> n0
-  
+
   (** val abs : z -> z **)
-  
+
   let abs = function
   | Zneg p -> Zpos p
   | x -> x
-  
-  (** val abs_nat : z -> nat **)
-  
-  let abs_nat = function
-  | Z0 -> O
-  | Zpos p -> Coq_Pos.to_nat p
-  | Zneg p -> Coq_Pos.to_nat p
-  
-  (** val abs_N : z -> n **)
-  
-  let abs_N = function
-  | Z0 -> N0
-  | Zpos p -> Npos p
-  | Zneg p -> Npos p
-  
-  (** val to_nat : z -> nat **)
-  
-  let to_nat = function
-  | Zpos p -> Coq_Pos.to_nat p
-  | _ -> O
-  
+
   (** val to_N : z -> n **)
-  
+
   let to_N = function
   | Zpos p -> Npos p
   | _ -> N0
-  
-  (** val of_nat : nat -> z **)
-  
-  let of_nat = function
-  | O -> Z0
-  | S n1 -> Zpos (Coq_Pos.of_succ_nat n1)
-  
-  (** val of_N : n -> z **)
-  
-  let of_N = function
-  | N0 -> Z0
-  | Npos p -> Zpos p
-  
-  (** val iter : z -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
-  
-  let iter n0 f x =
-    match n0 with
-    | Zpos p -> Coq_Pos.iter p f x
-    | _ -> x
-  
+
   (** val pos_div_eucl : positive -> z -> z * z **)
-  
+
   let rec pos_div_eucl a b =
     match a with
     | XI a' ->
       let q0,r = pos_div_eucl a' b in
       let r' = add (mul (Zpos (XO XH)) r) (Zpos XH) in
-      if gtb b r'
+      if ltb r' b
       then (mul (Zpos (XO XH)) q0),r'
       else (add (mul (Zpos (XO XH)) q0) (Zpos XH)),(sub r' b)
     | XO a' ->
       let q0,r = pos_div_eucl a' b in
       let r' = mul (Zpos (XO XH)) r in
-      if gtb b r'
+      if ltb r' b
       then (mul (Zpos (XO XH)) q0),r'
       else (add (mul (Zpos (XO XH)) q0) (Zpos XH)),(sub r' b)
-    | XH -> if geb b (Zpos (XO XH)) then Z0,(Zpos XH) else (Zpos XH),Z0
-  
+    | XH -> if leb (Zpos (XO XH)) b then Z0,(Zpos XH) else (Zpos XH),Z0
+
   (** val div_eucl : z -> z -> z * z **)
-  
+
   let div_eucl a b =
     match a with
     | Z0 -> Z0,Z0
     | Zpos a' ->
       (match b with
        | Z0 -> Z0,Z0
-       | Zpos p -> pos_div_eucl a' b
+       | Zpos _ -> pos_div_eucl a' b
        | Zneg b' ->
          let q0,r = pos_div_eucl a' (Zpos b') in
          (match r with
@@ -2320,131 +478,20 @@ module Z =
     | Zneg a' ->
       (match b with
        | Z0 -> Z0,Z0
-       | Zpos p ->
+       | Zpos _ ->
          let q0,r = pos_div_eucl a' b in
          (match r with
           | Z0 -> (opp q0),Z0
           | _ -> (opp (add q0 (Zpos XH))),(sub b r))
        | Zneg b' -> let q0,r = pos_div_eucl a' (Zpos b') in q0,(opp r))
-  
+
   (** val div : z -> z -> z **)
-  
+
   let div a b =
-    let q0,x = div_eucl a b in q0
-  
-  (** val modulo : z -> z -> z **)
-  
-  let modulo a b =
-    let x,r = div_eucl a b in r
-  
-  (** val quotrem : z -> z -> z * z **)
-  
-  let quotrem a b =
-    match a with
-    | Z0 -> Z0,Z0
-    | Zpos a0 ->
-      (match b with
-       | Z0 -> Z0,a
-       | Zpos b0 ->
-         let q0,r = N.pos_div_eucl a0 (Npos b0) in (of_N q0),(of_N r)
-       | Zneg b0 ->
-         let q0,r = N.pos_div_eucl a0 (Npos b0) in (opp (of_N q0)),(of_N r))
-    | Zneg a0 ->
-      (match b with
-       | Z0 -> Z0,a
-       | Zpos b0 ->
-         let q0,r = N.pos_div_eucl a0 (Npos b0) in
-         (opp (of_N q0)),(opp (of_N r))
-       | Zneg b0 ->
-         let q0,r = N.pos_div_eucl a0 (Npos b0) in (of_N q0),(opp (of_N r)))
-  
-  (** val quot : z -> z -> z **)
-  
-  let quot a b =
-    fst (quotrem a b)
-  
-  (** val rem : z -> z -> z **)
-  
-  let rem a b =
-    snd (quotrem a b)
-  
-  (** val even : z -> bool **)
-  
-  let even = function
-  | Z0 -> true
-  | Zpos p ->
-    (match p with
-     | XO p2 -> true
-     | _ -> false)
-  | Zneg p ->
-    (match p with
-     | XO p2 -> true
-     | _ -> false)
-  
-  (** val odd : z -> bool **)
-  
-  let odd = function
-  | Z0 -> false
-  | Zpos p ->
-    (match p with
-     | XO p2 -> false
-     | _ -> true)
-  | Zneg p ->
-    (match p with
-     | XO p2 -> false
-     | _ -> true)
-  
-  (** val div2 : z -> z **)
-  
-  let div2 = function
-  | Z0 -> Z0
-  | Zpos p ->
-    (match p with
-     | XH -> Z0
-     | _ -> Zpos (Coq_Pos.div2 p))
-  | Zneg p -> Zneg (Coq_Pos.div2_up p)
-  
-  (** val quot2 : z -> z **)
-  
-  let quot2 = function
-  | Z0 -> Z0
-  | Zpos p ->
-    (match p with
-     | XH -> Z0
-     | _ -> Zpos (Coq_Pos.div2 p))
-  | Zneg p ->
-    (match p with
-     | XH -> Z0
-     | _ -> Zneg (Coq_Pos.div2 p))
-  
-  (** val log2 : z -> z **)
-  
-  let log2 = function
-  | Zpos p2 ->
-    (match p2 with
-     | XI p -> Zpos (Coq_Pos.size p)
-     | XO p -> Zpos (Coq_Pos.size p)
-     | XH -> Z0)
-  | _ -> Z0
-  
-  (** val sqrtrem : z -> z * z **)
-  
-  let sqrtrem = function
-  | Zpos p ->
-    let s,m = Coq_Pos.sqrtrem p in
-    (match m with
-     | Coq_Pos.IsPos r -> (Zpos s),(Zpos r)
-     | _ -> (Zpos s),Z0)
-  | _ -> Z0,Z0
-  
-  (** val sqrt : z -> z **)
-  
-  let sqrt = function
-  | Zpos p -> Zpos (Coq_Pos.sqrt p)
-  | _ -> Z0
-  
+    let q0,_ = div_eucl a b in q0
+
   (** val gcd : z -> z -> z **)
-  
+
   let gcd a b =
     match a with
     | Z0 -> abs b
@@ -2458,316 +505,6 @@ module Z =
        | Z0 -> abs a
        | Zpos b0 -> Zpos (Coq_Pos.gcd a0 b0)
        | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0))
-  
-  (** val ggcd : z -> z -> z * (z * z) **)
-  
-  let ggcd a b =
-    match a with
-    | Z0 -> (abs b),(Z0,(sgn b))
-    | Zpos a0 ->
-      (match b with
-       | Z0 -> (abs a),((sgn a),Z0)
-       | Zpos b0 ->
-         let g,p = Coq_Pos.ggcd a0 b0 in
-         let aa,bb = p in (Zpos g),((Zpos aa),(Zpos bb))
-       | Zneg b0 ->
-         let g,p = Coq_Pos.ggcd a0 b0 in
-         let aa,bb = p in (Zpos g),((Zpos aa),(Zneg bb)))
-    | Zneg a0 ->
-      (match b with
-       | Z0 -> (abs a),((sgn a),Z0)
-       | Zpos b0 ->
-         let g,p = Coq_Pos.ggcd a0 b0 in
-         let aa,bb = p in (Zpos g),((Zneg aa),(Zpos bb))
-       | Zneg b0 ->
-         let g,p = Coq_Pos.ggcd a0 b0 in
-         let aa,bb = p in (Zpos g),((Zneg aa),(Zneg bb)))
-  
-  (** val testbit : z -> z -> bool **)
-  
-  let testbit a = function
-  | Z0 -> odd a
-  | Zpos p ->
-    (match a with
-     | Z0 -> false
-     | Zpos a0 -> Coq_Pos.testbit a0 (Npos p)
-     | Zneg a0 -> negb (N.testbit (Coq_Pos.pred_N a0) (Npos p)))
-  | Zneg p -> false
-  
-  (** val shiftl : z -> z -> z **)
-  
-  let shiftl a = function
-  | Z0 -> a
-  | Zpos p -> Coq_Pos.iter p (mul (Zpos (XO XH))) a
-  | Zneg p -> Coq_Pos.iter p div2 a
-  
-  (** val shiftr : z -> z -> z **)
-  
-  let shiftr a n0 =
-    shiftl a (opp n0)
-  
-  (** val coq_lor : z -> z -> z **)
-  
-  let coq_lor a b =
-    match a with
-    | Z0 -> b
-    | Zpos a0 ->
-      (match b with
-       | Z0 -> a
-       | Zpos b0 -> Zpos (Coq_Pos.coq_lor a0 b0)
-       | Zneg b0 -> Zneg (N.succ_pos (N.ldiff (Coq_Pos.pred_N b0) (Npos a0))))
-    | Zneg a0 ->
-      (match b with
-       | Z0 -> a
-       | Zpos b0 -> Zneg (N.succ_pos (N.ldiff (Coq_Pos.pred_N a0) (Npos b0)))
-       | Zneg b0 ->
-         Zneg
-           (N.succ_pos (N.coq_land (Coq_Pos.pred_N a0) (Coq_Pos.pred_N b0))))
-  
-  (** val coq_land : z -> z -> z **)
-  
-  let coq_land a b =
-    match a with
-    | Z0 -> Z0
-    | Zpos a0 ->
-      (match b with
-       | Z0 -> Z0
-       | Zpos b0 -> of_N (Coq_Pos.coq_land a0 b0)
-       | Zneg b0 -> of_N (N.ldiff (Npos a0) (Coq_Pos.pred_N b0)))
-    | Zneg a0 ->
-      (match b with
-       | Z0 -> Z0
-       | Zpos b0 -> of_N (N.ldiff (Npos b0) (Coq_Pos.pred_N a0))
-       | Zneg b0 ->
-         Zneg
-           (N.succ_pos (N.coq_lor (Coq_Pos.pred_N a0) (Coq_Pos.pred_N b0))))
-  
-  (** val ldiff : z -> z -> z **)
-  
-  let ldiff a b =
-    match a with
-    | Z0 -> Z0
-    | Zpos a0 ->
-      (match b with
-       | Z0 -> a
-       | Zpos b0 -> of_N (Coq_Pos.ldiff a0 b0)
-       | Zneg b0 -> of_N (N.coq_land (Npos a0) (Coq_Pos.pred_N b0)))
-    | Zneg a0 ->
-      (match b with
-       | Z0 -> a
-       | Zpos b0 ->
-         Zneg (N.succ_pos (N.coq_lor (Coq_Pos.pred_N a0) (Npos b0)))
-       | Zneg b0 -> of_N (N.ldiff (Coq_Pos.pred_N b0) (Coq_Pos.pred_N a0)))
-  
-  (** val coq_lxor : z -> z -> z **)
-  
-  let coq_lxor a b =
-    match a with
-    | Z0 -> b
-    | Zpos a0 ->
-      (match b with
-       | Z0 -> a
-       | Zpos b0 -> of_N (Coq_Pos.coq_lxor a0 b0)
-       | Zneg b0 ->
-         Zneg (N.succ_pos (N.coq_lxor (Npos a0) (Coq_Pos.pred_N b0))))
-    | Zneg a0 ->
-      (match b with
-       | Z0 -> a
-       | Zpos b0 ->
-         Zneg (N.succ_pos (N.coq_lxor (Coq_Pos.pred_N a0) (Npos b0)))
-       | Zneg b0 -> of_N (N.coq_lxor (Coq_Pos.pred_N a0) (Coq_Pos.pred_N b0)))
-  
-  (** val eq_dec : z -> z -> bool **)
-  
-  let eq_dec x y =
-    match x with
-    | Z0 ->
-      (match y with
-       | Z0 -> true
-       | _ -> false)
-    | Zpos x0 ->
-      (match y with
-       | Zpos p2 -> Coq_Pos.eq_dec x0 p2
-       | _ -> false)
-    | Zneg x0 ->
-      (match y with
-       | Zneg p2 -> Coq_Pos.eq_dec x0 p2
-       | _ -> false)
-  
-  module BootStrap = 
-   struct 
-    
-   end
-  
-  module OrderElts = 
-   struct 
-    type t = z
-   end
-  
-  module OrderTac = MakeOrderTac(OrderElts)
-  
-  (** val sqrt_up : z -> z **)
-  
-  let sqrt_up a =
-    match compare Z0 a with
-    | Lt -> succ (sqrt (pred a))
-    | _ -> Z0
-  
-  (** val log2_up : z -> z **)
-  
-  let log2_up a =
-    match compare (Zpos XH) a with
-    | Lt -> succ (log2 (pred a))
-    | _ -> Z0
-  
-  module NZDivP = 
-   struct 
-    
-   end
-  
-  module Quot2Div = 
-   struct 
-    (** val div : z -> z -> z **)
-    
-    let div =
-      quot
-    
-    (** val modulo : z -> z -> z **)
-    
-    let modulo =
-      rem
-   end
-  
-  module NZQuot = 
-   struct 
-    
-   end
-  
-  (** val lcm : z -> z -> z **)
-  
-  let lcm a b =
-    abs (mul a (div b (gcd a b)))
-  
-  (** val b2z : bool -> z **)
-  
-  let b2z = function
-  | true -> Zpos XH
-  | false -> Z0
-  
-  (** val setbit : z -> z -> z **)
-  
-  let setbit a n0 =
-    coq_lor a (shiftl (Zpos XH) n0)
-  
-  (** val clearbit : z -> z -> z **)
-  
-  let clearbit a n0 =
-    ldiff a (shiftl (Zpos XH) n0)
-  
-  (** val lnot : z -> z **)
-  
-  let lnot a =
-    pred (opp a)
-  
-  (** val ones : z -> z **)
-  
-  let ones n0 =
-    pred (shiftl (Zpos XH) n0)
-  
-  module T = 
-   struct 
-    
-   end
-  
-  module ORev = 
-   struct 
-    type t = z
-   end
-  
-  module MRev = 
-   struct 
-    (** val max : z -> z -> z **)
-    
-    let max x y =
-      min y x
-   end
-  
-  module MPRev = MaxLogicalProperties(ORev)(MRev)
-  
-  module P = 
-   struct 
-    (** val max_case_strong :
-        z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-        -> 'a1 **)
-    
-    let max_case_strong n0 m compat hl hr =
-      let c = compSpec2Type n0 m (compare n0 m) in
-      (match c with
-       | CompGtT -> compat n0 (max n0 m) __ (hl __)
-       | _ -> compat m (max n0 m) __ (hr __))
-    
-    (** val max_case :
-        z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **)
-    
-    let max_case n0 m x x0 x1 =
-      max_case_strong n0 m x (fun _ -> x0) (fun _ -> x1)
-    
-    (** val max_dec : z -> z -> bool **)
-    
-    let max_dec n0 m =
-      max_case n0 m (fun x y _ h0 -> h0) true false
-    
-    (** val min_case_strong :
-        z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-        -> 'a1 **)
-    
-    let min_case_strong n0 m compat hl hr =
-      let c = compSpec2Type n0 m (compare n0 m) in
-      (match c with
-       | CompGtT -> compat m (min n0 m) __ (hr __)
-       | _ -> compat n0 (min n0 m) __ (hl __))
-    
-    (** val min_case :
-        z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **)
-    
-    let min_case n0 m x x0 x1 =
-      min_case_strong n0 m x (fun _ -> x0) (fun _ -> x1)
-    
-    (** val min_dec : z -> z -> bool **)
-    
-    let min_dec n0 m =
-      min_case n0 m (fun x y _ h0 -> h0) true false
-   end
-  
-  (** val max_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
-  
-  let max_case_strong n0 m x x0 =
-    P.max_case_strong n0 m (fun x1 y _ x2 -> x2) x x0
-  
-  (** val max_case : z -> z -> 'a1 -> 'a1 -> 'a1 **)
-  
-  let max_case n0 m x x0 =
-    max_case_strong n0 m (fun _ -> x) (fun _ -> x0)
-  
-  (** val max_dec : z -> z -> bool **)
-  
-  let max_dec =
-    P.max_dec
-  
-  (** val min_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
-  
-  let min_case_strong n0 m x x0 =
-    P.min_case_strong n0 m (fun x1 y _ x2 -> x2) x x0
-  
-  (** val min_case : z -> z -> 'a1 -> 'a1 -> 'a1 **)
-  
-  let min_case n0 m x x0 =
-    min_case_strong n0 m (fun _ -> x) (fun _ -> x0)
-  
-  (** val min_dec : z -> z -> bool **)
-  
-  let min_dec =
-    P.min_dec
  end
 
 (** val zeq_bool : z -> z -> bool **)
@@ -2818,9 +555,9 @@ let rec peq ceqb p p' =
 (** val mkPinj : positive -> 'a1 pol -> 'a1 pol **)
 
 let mkPinj j p = match p with
-| Pc c -> p
+| Pc _ -> p
 | Pinj (j', q0) -> Pinj ((Coq_Pos.add j j'), q0)
-| PX (p2, p3, p4) -> Pinj (j, p)
+| PX (_, _, _) -> Pinj (j, p)
 
 (** val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol **)
 
@@ -2831,12 +568,13 @@ let mkPinj_pred j p =
   | XH -> p
 
 (** val mkPX :
-    'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **)
+    'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1
+    pol **)
 
 let mkPX cO ceqb p i q0 =
   match p with
   | Pc c -> if ceqb c cO then mkPinj XH q0 else PX (p, i, q0)
-  | Pinj (p2, p3) -> PX (p, i, q0)
+  | Pinj (_, _) -> PX (p, i, q0)
   | PX (p', i', q') ->
     if peq ceqb q' (p0 cO)
     then PX (p', (Coq_Pos.add i' i), q0)
@@ -2893,8 +631,8 @@ let rec paddI cadd pop q0 j = function
    | XH -> PX (p2, i, (pop q' q0)))
 
 (** val psubI :
-    ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) ->
-    'a1 pol -> positive -> 'a1 pol -> 'a1 pol **)
+    ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol)
+    -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **)
 
 let rec psubI cadd copp pop q0 j = function
 | Pc c -> mkPinj j (paddC cadd (popp copp q0) c)
@@ -2911,11 +649,11 @@ let rec psubI cadd copp pop q0 j = function
    | XH -> PX (p2, i, (pop q' q0)))
 
 (** val paddX :
-    'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol
-    -> positive -> 'a1 pol -> 'a1 pol **)
+    'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1
+    pol -> positive -> 'a1 pol -> 'a1 pol **)
 
 let rec paddX cO ceqb pop p' i' p = match p with
-| Pc c -> PX (p', i', p)
+| Pc _ -> PX (p', i', p)
 | Pinj (j, q') ->
   (match j with
    | XI j0 -> PX (p', i', (Pinj ((XO j0), q')))
@@ -2928,15 +666,16 @@ let rec paddX cO ceqb pop p' i' p = match p with
    | Zneg k -> mkPX cO ceqb (paddX cO ceqb pop p' k p2) i q')
 
 (** val psubX :
-    'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1
-    pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **)
+    'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol ->
+    'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **)
 
 let rec psubX cO copp ceqb pop p' i' p = match p with
-| Pc c -> PX ((popp copp p'), i', p)
+| Pc _ -> PX ((popp copp p'), i', p)
 | Pinj (j, q') ->
   (match j with
    | XI j0 -> PX ((popp copp p'), i', (Pinj ((XO j0), q')))
-   | XO j0 -> PX ((popp copp p'), i', (Pinj ((Coq_Pos.pred_double j0), q')))
+   | XO j0 ->
+     PX ((popp copp p'), i', (Pinj ((Coq_Pos.pred_double j0), q')))
    | XH -> PX ((popp copp p'), i', q'))
 | PX (p2, i, q') ->
   (match Z.pos_sub i i' with
@@ -2945,8 +684,8 @@ let rec psubX cO copp ceqb pop p' i' p = match p with
    | Zneg k -> mkPX cO ceqb (psubX cO copp ceqb pop p' k p2) i q')
 
 (** val padd :
-    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol
-    -> 'a1 pol **)
+    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1
+    pol -> 'a1 pol **)
 
 let rec padd cO cadd ceqb p = function
 | Pc c' -> paddC cadd p c'
@@ -2964,7 +703,8 @@ let rec padd cO cadd ceqb p = function
    | PX (p2, i, q0) ->
      (match Z.pos_sub i i' with
       | Z0 ->
-        mkPX cO ceqb (padd cO cadd ceqb p2 p'0) i (padd cO cadd ceqb q0 q')
+        mkPX cO ceqb (padd cO cadd ceqb p2 p'0) i
+          (padd cO cadd ceqb q0 q')
       | Zpos k ->
         mkPX cO ceqb (padd cO cadd ceqb (PX (p2, k, (p0 cO))) p'0) i'
           (padd cO cadd ceqb q0 q')
@@ -2973,8 +713,8 @@ let rec padd cO cadd ceqb p = function
           (padd cO cadd ceqb q0 q')))
 
 (** val psub :
-    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
-    -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **)
+    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) ->
+    ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **)
 
 let rec psub cO cadd csub copp ceqb p = function
 | Pc c' -> psubC csub p c'
@@ -2989,25 +729,27 @@ let rec psub cO cadd csub copp ceqb p = function
           (psub cO cadd csub copp ceqb (Pinj ((XO j0), q0)) q'))
       | XO j0 ->
         PX ((popp copp p'0), i',
-          (psub cO cadd csub copp ceqb (Pinj ((Coq_Pos.pred_double j0), q0))
-            q'))
-      | XH -> PX ((popp copp p'0), i', (psub cO cadd csub copp ceqb q0 q')))
+          (psub cO cadd csub copp ceqb (Pinj ((Coq_Pos.pred_double j0),
+            q0)) q'))
+      | XH ->
+        PX ((popp copp p'0), i', (psub cO cadd csub copp ceqb q0 q')))
    | PX (p2, i, q0) ->
      (match Z.pos_sub i i' with
       | Z0 ->
         mkPX cO ceqb (psub cO cadd csub copp ceqb p2 p'0) i
           (psub cO cadd csub copp ceqb q0 q')
       | Zpos k ->
-        mkPX cO ceqb (psub cO cadd csub copp ceqb (PX (p2, k, (p0 cO))) p'0)
-          i' (psub cO cadd csub copp ceqb q0 q')
+        mkPX cO ceqb
+          (psub cO cadd csub copp ceqb (PX (p2, k, (p0 cO))) p'0) i'
+          (psub cO cadd csub copp ceqb q0 q')
       | Zneg k ->
         mkPX cO ceqb
           (psubX cO copp ceqb (psub cO cadd csub copp ceqb) p'0 k p2) i
           (psub cO cadd csub copp ceqb q0 q')))
 
 (** val pmulC_aux :
-    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 ->
-    'a1 pol **)
+    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1
+    -> 'a1 pol **)
 
 let rec pmulC_aux cO cmul ceqb p c =
   match p with
@@ -3018,8 +760,8 @@ let rec pmulC_aux cO cmul ceqb p c =
       (pmulC_aux cO cmul ceqb q0 c)
 
 (** val pmulC :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol ->
-    'a1 -> 'a1 pol **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol
+    -> 'a1 -> 'a1 pol **)
 
 let pmulC cO cI cmul ceqb p c =
   if ceqb c cO
@@ -3027,8 +769,8 @@ let pmulC cO cI cmul ceqb p c =
   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 ->
-    'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol
+    -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **)
 
 let rec pmulI cO cI cmul ceqb pmul0 q0 j = function
 | Pc c -> mkPinj j (pmulC cO cI cmul ceqb q0 c)
@@ -3049,12 +791,13 @@ let rec pmulI cO cI cmul ceqb pmul0 q0 j = function
      mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 XH p') i' (pmul0 q' q0))
 
 (** val pmul :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **)
 
 let rec pmul cO cI cadd cmul ceqb p p'' = match p'' with
 | Pc c -> pmulC cO cI cmul ceqb p c
-| Pinj (j', q') -> pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' j' p
+| Pinj (j', q') ->
+  pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' j' p
 | PX (p', i', q') ->
   (match p with
    | Pc c -> pmulC cO cI cmul ceqb p'' c
@@ -3063,22 +806,24 @@ let rec pmul cO cI cadd cmul ceqb p p'' = match p'' with
        match j with
        | XI j0 -> pmul cO cI cadd cmul ceqb (Pinj ((XO j0), q0)) q'
        | XO j0 ->
-         pmul cO cI cadd cmul ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) q'
+         pmul cO cI cadd cmul ceqb (Pinj ((Coq_Pos.pred_double j0), q0))
+           q'
        | XH -> pmul cO cI cadd cmul ceqb q0 q'
      in
      mkPX cO ceqb (pmul cO cI cadd cmul ceqb p p') i' qQ'
    | PX (p2, i, q0) ->
      let qQ' = pmul cO cI cadd cmul ceqb q0 q' in
-     let pQ' = pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' XH p2 in
+     let pQ' = pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' XH p2
+     in
      let qP' = pmul cO cI cadd cmul ceqb (mkPinj XH q0) p' in
      let pP' = pmul cO cI cadd cmul ceqb p2 p' in
      padd cO cadd ceqb
-       (mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb pP' i (p0 cO)) qP') i'
-         (p0 cO)) (mkPX cO ceqb pQ' i qQ'))
+       (mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb pP' i (p0 cO)) qP')
+         i' (p0 cO)) (mkPX cO ceqb pQ' i qQ'))
 
 (** val psquare :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> bool) -> 'a1 pol -> 'a1 pol **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> bool) -> 'a1 pol -> 'a1 pol **)
 
 let rec psquare cO cI cadd cmul ceqb = function
 | Pc c -> Pc (cmul c c)
@@ -3107,9 +852,9 @@ let mk_X cO cI j =
   mkPinj_pred j (mkX cO cI)
 
 (** val ppow_pos :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1
-    pol **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive
+    -> 'a1 pol **)
 
 let rec ppow_pos cO cI cadd cmul ceqb subst_l res p = function
 | XI p3 ->
@@ -3123,16 +868,17 @@ let rec ppow_pos cO cI cadd cmul ceqb subst_l res p = function
 | XH -> subst_l (pmul cO cI cadd cmul ceqb res p)
 
 (** val ppow_N :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol **)
 
 let ppow_N cO cI cadd cmul ceqb subst_l p = function
 | N0 -> p1 cI
 | Npos p2 -> ppow_pos cO cI cadd cmul ceqb subst_l (p1 cI) p p2
 
 (** val norm_aux :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr ->
+    'a1 pol **)
 
 let rec norm_aux cO cI cadd cmul csub copp ceqb = function
 | PEc c -> Pc c
@@ -3153,7 +899,8 @@ let rec norm_aux cO cI cadd cmul csub copp ceqb = function
         padd cO cadd ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1)
           (norm_aux cO cI cadd cmul csub copp ceqb pe2)))
 | PEsub (pe1, pe2) ->
-  psub cO cadd csub copp ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1)
+  psub cO cadd csub copp ceqb
+    (norm_aux cO cI cadd cmul csub copp ceqb pe1)
     (norm_aux cO cI cadd cmul csub copp ceqb pe2)
 | PEmul (pe1, pe2) ->
   pmul cO cI cadd cmul ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1)
@@ -3185,9 +932,9 @@ let rec map_bformula fct = function
 | N f0 -> N (map_bformula fct f0)
 | I (f1, f2) -> I ((map_bformula fct f1), (map_bformula fct f2))
 
-type 'term' clause = 'term' list
+type 'x clause = 'x list
 
-type 'term' cnf = 'term' clause list
+type 'x cnf = 'x clause list
 
 (** val tt : 'a1 cnf **)
 
@@ -3200,52 +947,52 @@ let ff =
   []::[]
 
 (** val add_term :
-    ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> 'a1
-    clause option **)
+    ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause ->
+    'a1 clause option **)
 
-let rec add_term unsat deduce t1 = function
+let rec add_term unsat deduce t0 = function
 | [] ->
-  (match deduce t1 t1 with
-   | Some u -> if unsat u then None else Some (t1::[])
-   | None -> Some (t1::[]))
+  (match deduce t0 t0 with
+   | Some u -> if unsat u then None else Some (t0::[])
+   | None -> Some (t0::[]))
 | t'::cl0 ->
-  (match deduce t1 t' with
+  (match deduce t0 t' with
    | Some u ->
      if unsat u
      then None
-     else (match add_term unsat deduce t1 cl0 with
+     else (match add_term unsat deduce t0 cl0 with
            | Some cl' -> Some (t'::cl')
            | None -> None)
    | None ->
-     (match add_term unsat deduce t1 cl0 with
+     (match add_term unsat deduce t0 cl0 with
       | Some cl' -> Some (t'::cl')
       | None -> None))
 
 (** val or_clause :
-    ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 clause
-    -> 'a1 clause option **)
+    ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1
+    clause -> 'a1 clause option **)
 
 let rec or_clause unsat deduce cl1 cl2 =
   match cl1 with
   | [] -> Some cl2
-  | t1::cl ->
-    (match add_term unsat deduce t1 cl2 with
+  | t0::cl ->
+    (match add_term unsat deduce t0 cl2 with
      | Some cl' -> or_clause unsat deduce cl cl'
      | None -> None)
 
 (** val or_clause_cnf :
-    ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf ->
-    'a1 cnf **)
+    ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf
+    -> 'a1 cnf **)
 
-let or_clause_cnf unsat deduce t1 f =
+let or_clause_cnf unsat deduce t0 f =
   fold_right (fun e acc ->
-    match or_clause unsat deduce t1 e with
+    match or_clause unsat deduce t0 e with
     | Some cl -> cl::acc
     | None -> acc) [] f
 
 (** val or_cnf :
-    ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> 'a1
-    cnf **)
+    ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf ->
+    'a1 cnf **)
 
 let rec or_cnf unsat deduce f f' =
   match f with
@@ -3259,8 +1006,8 @@ let and_cnf f1 f2 =
   app f1 f2
 
 (** val xcnf :
-    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1
-    -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf **)
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) ->
+    ('a1 -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf **)
 
 let rec xcnf unsat deduce normalise0 negate0 pol0 = function
 | TT -> if pol0 then tt else ff
@@ -3300,9 +1047,9 @@ let rec cnf_checker checker f l =
      | c::l0 -> if checker e c then cnf_checker checker f0 l0 else false)
 
 (** val tauto_checker :
-    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1
-    -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 list ->
-    bool **)
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) ->
+    ('a1 -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3
+    list -> bool **)
 
 let tauto_checker unsat deduce normalise0 negate0 checker f w =
   cnf_checker checker (xcnf unsat deduce normalise0 negate0 true f) w
@@ -3335,18 +1082,18 @@ let opMult o o' =
   | Equal -> Some Equal
   | NonEqual ->
     (match o' with
-     | Strict -> None
-     | NonStrict -> None
-     | x -> Some x)
+     | Equal -> Some Equal
+     | NonEqual -> Some NonEqual
+     | _ -> None)
   | Strict ->
     (match o' with
      | NonEqual -> None
      | _ -> Some o')
   | NonStrict ->
     (match o' with
+     | Equal -> Some Equal
      | NonEqual -> None
-     | Strict -> Some NonStrict
-     | x -> Some x)
+     | _ -> Some NonStrict)
 
 (** val opAdd : op1 -> op1 -> op1 option **)
 
@@ -3394,8 +1141,8 @@ let map_option2 f o o' =
   | None -> None
 
 (** val pexpr_times_nformula :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option **)
 
 let pexpr_times_nformula cO cI cplus ctimes ceqb e = function
 | ef,o ->
@@ -3404,8 +1151,8 @@ let pexpr_times_nformula cO cI cplus ctimes ceqb e = function
    | _ -> None)
 
 (** val nformula_times_nformula :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option **)
 
 let nformula_times_nformula cO cI cplus ctimes ceqb f1 f2 =
   let e1,o1 = f1 in
@@ -3414,8 +1161,8 @@ let nformula_times_nformula cO cI cplus ctimes ceqb f1 f2 =
     (opMult o1 o2)
 
 (** val nformula_plus_nformula :
-    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1
-    nFormula -> 'a1 nFormula option **)
+    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula ->
+    'a1 nFormula -> 'a1 nFormula option **)
 
 let nformula_plus_nformula cO cplus ceqb f1 f2 =
   let e1,o1 = f1 in
@@ -3423,9 +1170,9 @@ let nformula_plus_nformula cO cplus ceqb f1 f2 =
   map_option (fun x -> Some ((padd cO cplus ceqb e1 e2),x)) (opAdd o1 o2)
 
 (** val eval_Psatz :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1
-    nFormula option **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz
+    -> 'a1 nFormula option **)
 
 let rec eval_Psatz cO cI cplus ctimes ceqb cleb l = function
 | PsatzIn n0 -> Some (nth n0 l ((Pc cO),Equal))
@@ -3460,9 +1207,9 @@ let check_inconsistent cO ceqb cleb = function
    | _ -> false)
 
 (** val check_normalised_formulas :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz ->
-    bool **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz
+    -> bool **)
 
 let check_normalised_formulas cO cI cplus ctimes ceqb cleb l cm =
   match eval_Psatz cO cI cplus ctimes ceqb cleb l cm with
@@ -3479,51 +1226,41 @@ type op2 =
 
 type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr }
 
-(** val flhs : 'a1 formula -> 'a1 pExpr **)
-
-let flhs x = x.flhs
-
-(** val fop : 'a1 formula -> op2 **)
-
-let fop x = x.fop
-
-(** val frhs : 'a1 formula -> 'a1 pExpr **)
-
-let frhs x = x.frhs
-
 (** val norm :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr ->
+    'a1 pol **)
 
 let norm cO cI cplus ctimes cminus copp ceqb =
   norm_aux cO cI cplus ctimes cminus copp ceqb
 
 (** val psub0 :
-    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
-    -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **)
+    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) ->
+    ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **)
 
 let psub0 cO cplus cminus copp ceqb =
   psub cO cplus cminus copp ceqb
 
 (** val padd0 :
-    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol
-    -> 'a1 pol **)
+    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1
+    pol -> 'a1 pol **)
 
 let padd0 cO cplus ceqb =
   padd cO cplus ceqb
 
 (** val xnormalise :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1
-    nFormula list **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula ->
+    'a1 nFormula list **)
 
-let xnormalise cO cI cplus ctimes cminus copp ceqb t1 =
-  let { flhs = lhs; fop = o; frhs = rhs } = t1 in
+let xnormalise cO cI cplus ctimes cminus copp ceqb t0 =
+  let { flhs = lhs; fop = o; frhs = rhs } = t0 in
   let lhs0 = norm cO cI cplus ctimes cminus copp ceqb lhs in
   let rhs0 = norm cO cI cplus ctimes cminus copp ceqb rhs in
   (match o with
    | OpEq ->
-     ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO cplus
+     ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO
+                                                               cplus
                                                                cminus copp
                                                                ceqb rhs0
                                                                lhs0),Strict)::[])
@@ -3534,26 +1271,27 @@ let xnormalise cO cI cplus ctimes cminus copp ceqb t1 =
    | OpGt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),NonStrict)::[])
 
 (** val cnf_normalise :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1
-    nFormula cnf **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula ->
+    'a1 nFormula cnf **)
 
-let cnf_normalise cO cI cplus ctimes cminus copp ceqb t1 =
-  map (fun x -> x::[]) (xnormalise cO cI cplus ctimes cminus copp ceqb t1)
+let cnf_normalise cO cI cplus ctimes cminus copp ceqb t0 =
+  map (fun x -> x::[]) (xnormalise cO cI cplus ctimes cminus copp ceqb t0)
 
 (** val xnegate :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1
-    nFormula list **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula ->
+    'a1 nFormula list **)
 
-let xnegate cO cI cplus ctimes cminus copp ceqb t1 =
-  let { flhs = lhs; fop = o; frhs = rhs } = t1 in
+let xnegate cO cI cplus ctimes cminus copp ceqb t0 =
+  let { flhs = lhs; fop = o; frhs = rhs } = t0 in
   let lhs0 = norm cO cI cplus ctimes cminus copp ceqb lhs in
   let rhs0 = norm cO cI cplus ctimes cminus copp ceqb rhs in
   (match o with
    | OpEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Equal)::[]
    | OpNEq ->
-     ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO cplus
+     ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO
+                                                               cplus
                                                                cminus copp
                                                                ceqb rhs0
                                                                lhs0),Strict)::[])
@@ -3563,12 +1301,12 @@ let xnegate cO cI cplus ctimes cminus copp ceqb t1 =
    | OpGt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::[])
 
 (** val cnf_negate :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-    -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1
-    nFormula cnf **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 ->
+    'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula ->
+    'a1 nFormula cnf **)
 
-let cnf_negate cO cI cplus ctimes cminus copp ceqb t1 =
-  map (fun x -> x::[]) (xnegate cO cI cplus ctimes cminus copp ceqb t1)
+let cnf_negate cO cI cplus ctimes cminus copp ceqb t0 =
+  map (fun x -> x::[]) (xnegate cO cI cplus ctimes cminus copp ceqb t0)
 
 (** val xdenorm : positive -> 'a1 pol -> 'a1 pExpr **)
 
@@ -3602,14 +1340,14 @@ let map_Formula c_of_S f =
   { flhs = (map_PExpr c_of_S l); fop = o; frhs = (map_PExpr c_of_S r) }
 
 (** val simpl_cone :
-    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz ->
-    'a1 psatz **)
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz
+    -> 'a1 psatz **)
 
 let simpl_cone cO cI ctimes ceqb e = match e with
-| PsatzSquare t1 ->
-  (match t1 with
+| PsatzSquare t0 ->
+  (match t0 with
    | Pc c -> if ceqb cO c then PsatzZ else PsatzC (ctimes c c)
-   | _ -> PsatzSquare t1)
+   | _ -> PsatzSquare t0)
 | PsatzMulE (t1, t2) ->
   (match t1 with
    | PsatzMulE (x, x0) ->
@@ -3641,7 +1379,8 @@ let simpl_cone cO cI ctimes ceqb e = match e with
             | PsatzC p2 -> PsatzMulE ((PsatzC (ctimes c p2)), x)
             | _ -> if ceqb cI c then t2 else PsatzMulE (t1, t2)))
       | PsatzAdd (y, z0) ->
-        PsatzAdd ((PsatzMulE ((PsatzC c), y)), (PsatzMulE ((PsatzC c), z0)))
+        PsatzAdd ((PsatzMulE ((PsatzC c), y)), (PsatzMulE ((PsatzC c),
+          z0)))
       | PsatzC c0 -> PsatzC (ctimes c c0)
       | PsatzZ -> PsatzZ
       | _ -> if ceqb cI c then t2 else PsatzMulE (t1, t2))
@@ -3683,7 +1422,8 @@ let qle_bool x y =
 (** val qplus : q -> q -> q **)
 
 let qplus x y =
-  { qnum = (Z.add (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)));
+  { qnum =
+    (Z.add (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)));
     qden = (Coq_Pos.mul x.qden y.qden) }
 
 (** val qmult : q -> q -> q **)
@@ -3711,8 +1451,8 @@ let qinv x =
 
 (** val qpower_positive : q -> positive -> q **)
 
-let qpower_positive q0 p =
-  pow_pos qmult q0 p
+let qpower_positive =
+  pow_pos qmult
 
 (** val qpower : q -> z -> q **)
 
@@ -3721,12 +1461,12 @@ let qpower q0 = function
 | Zpos p -> qpower_positive q0 p
 | Zneg p -> qinv (qpower_positive q0 p)
 
-type 'a t0 =
+type 'a t =
 | Empty
 | Leaf of 'a
-| Node of 'a t0 * 'a * 'a t0
+| Node of 'a t * 'a * 'a t
 
-(** val find : 'a1 -> 'a1 t0 -> positive -> 'a1 **)
+(** val find : 'a1 -> 'a1 t -> positive -> 'a1 **)
 
 let rec find default vm p =
   match vm with
@@ -3738,6 +1478,29 @@ let rec find default vm p =
      | XO p2 -> find default l p2
      | XH -> e)
 
+(** val singleton : 'a1 -> positive -> 'a1 -> 'a1 t **)
+
+let rec singleton default x v =
+  match x with
+  | XI p -> Node (Empty, default, (singleton default p v))
+  | XO p -> Node ((singleton default p v), default, Empty)
+  | XH -> Leaf v
+
+(** val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t **)
+
+let rec vm_add default x v = function
+| Empty -> singleton default x v
+| Leaf vl ->
+  (match x with
+   | XI p -> Node (Empty, vl, (singleton default p v))
+   | XO p -> Node ((singleton default p v), vl, Empty)
+   | XH -> Leaf v)
+| Node (l, o, r) ->
+  (match x with
+   | XI p -> Node (l, o, (vm_add default p v r))
+   | XO p -> Node ((vm_add default p v l), o, r)
+   | XH -> Node (l, v, r))
+
 type zWitness = z psatz
 
 (** val zWeakChecker : z nFormula list -> z psatz -> bool **)
@@ -3762,8 +1525,8 @@ let norm0 =
 
 (** val xnormalise0 : z formula -> z nFormula list **)
 
-let xnormalise0 t1 =
-  let { flhs = lhs; fop = o; frhs = rhs } = t1 in
+let xnormalise0 t0 =
+  let { flhs = lhs; fop = o; frhs = rhs } = t0 in
   let lhs0 = norm0 lhs in
   let rhs0 = norm0 rhs in
   (match o with
@@ -3780,13 +1543,13 @@ let xnormalise0 t1 =
 
 (** val normalise : z formula -> z nFormula cnf **)
 
-let normalise t1 =
-  map (fun x -> x::[]) (xnormalise0 t1)
+let normalise t0 =
+  map (fun x -> x::[]) (xnormalise0 t0)
 
 (** val xnegate0 : z formula -> z nFormula list **)
 
-let xnegate0 t1 =
-  let { flhs = lhs; fop = o; frhs = rhs } = t1 in
+let xnegate0 t0 =
+  let { flhs = lhs; fop = o; frhs = rhs } = t0 in
   let lhs0 = norm0 lhs in
   let rhs0 = norm0 rhs in
   (match o with
@@ -3803,8 +1566,8 @@ let xnegate0 t1 =
 
 (** val negate : z formula -> z nFormula cnf **)
 
-let negate t1 =
-  map (fun x -> x::[]) (xnegate0 t1)
+let negate t0 =
+  map (fun x -> x::[]) (xnegate0 t0)
 
 (** val zunsat : z nFormula -> bool **)
 
@@ -3839,8 +1602,8 @@ let zgcdM x y =
 
 let rec zgcd_pol = function
 | Pc c -> Z0,c
-| Pinj (p2, p3) -> zgcd_pol p3
-| PX (p2, p3, q0) ->
+| Pinj (_, p2) -> zgcd_pol p2
+| PX (p2, _, q0) ->
   let g1,c1 = zgcd_pol p2 in
   let g2,c2 = zgcd_pol q0 in (zgcdM (zgcdM g1 c1) g2),c2
 
@@ -3872,7 +1635,8 @@ let genCuttingPlane = function
      then None
      else Some ((makeCuttingPlane e),Equal)
    | NonEqual -> Some ((e,Z0),op)
-   | Strict -> Some ((makeCuttingPlane (psubC Z.sub e (Zpos XH))),NonStrict)
+   | Strict ->
+     Some ((makeCuttingPlane (psubC Z.sub e (Zpos XH))),NonStrict)
    | NonStrict -> Some ((makeCuttingPlane e),NonStrict))
 
 (** val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula **)
@@ -3966,8 +1730,8 @@ let qnormalise =
 (** val qnegate : q formula -> q nFormula cnf **)
 
 let qnegate =
-  cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus
-    qmult qminus qopp qeq_bool
+  cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH }
+    qplus qmult qminus qopp qeq_bool
 
 (** val qunsat : q nFormula -> bool **)
 
@@ -4025,8 +1789,8 @@ let rnormalise =
 (** val rnegate : q formula -> q nFormula cnf **)
 
 let rnegate =
-  cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus
-    qmult qminus qopp qeq_bool
+  cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH }
+    qplus qmult qminus qopp qeq_bool
 
 (** val runsat : q nFormula -> bool **)
 
@@ -4043,4 +1807,3 @@ let rdeduce =
 let rTautoChecker f w =
   tauto_checker runsat rdeduce rnormalise rnegate rWeakChecker
     (map_bformula (map_Formula q_of_Rcst) f) w
-
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index bcd61f39b..beb042f49 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -1,15 +1,9 @@
-type __ = Obj.t
-
 val negb : bool -> bool
 
 type nat =
 | O
 | S of nat
 
-val fst : ('a1 * 'a2) -> 'a1
-
-val snd : ('a1 * 'a2) -> 'a2
-
 val app : 'a1 list -> 'a1 list -> 'a1 list
 
 type comparison =
@@ -19,24 +13,7 @@ type comparison =
 
 val compOpp : comparison -> comparison
 
-type compareSpecT =
-| CompEqT
-| CompLtT
-| CompGtT
-
-val compareSpec2Type : comparison -> compareSpecT
-
-type 'a compSpecT = compareSpecT
-
-val compSpec2Type : 'a1 -> 'a1 -> comparison -> 'a1 compSpecT
-
-type 'a sig0 =
-  'a
-  (* singleton inductive, whose constructor was exist *)
-
-val plus : nat -> nat -> nat
-
-val nat_iter : nat -> ('a1 -> 'a1) -> 'a1 -> 'a1
+val add : nat -> nat -> nat
 
 type positive =
 | XI of positive
@@ -52,560 +29,59 @@ type z =
 | Zpos of positive
 | Zneg of positive
 
-module type TotalOrder' = 
- sig 
-  type t 
- end
-
-module MakeOrderTac : 
- functor (O:TotalOrder') ->
- sig 
-  
- end
-
-module MaxLogicalProperties : 
- functor (O:TotalOrder') ->
- functor (M:sig 
-  val max : O.t -> O.t -> O.t
- end) ->
- sig 
-  module T : 
-   sig 
-    
-   end
- end
-
-module Pos : 
- sig 
-  type t = positive
-  
-  val succ : positive -> positive
-  
-  val add : positive -> positive -> positive
-  
-  val add_carry : positive -> positive -> positive
-  
-  val pred_double : positive -> positive
-  
-  val pred : positive -> positive
-  
-  val pred_N : positive -> n
-  
+module Pos :
+ sig
   type mask =
   | IsNul
   | IsPos of positive
   | IsNeg
-  
-  val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1
-  
-  val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1
-  
-  val succ_double_mask : mask -> mask
-  
-  val double_mask : mask -> mask
-  
-  val double_pred_mask : positive -> mask
-  
-  val pred_mask : mask -> mask
-  
-  val sub_mask : positive -> positive -> mask
-  
-  val sub_mask_carry : positive -> positive -> mask
-  
-  val sub : positive -> positive -> positive
-  
-  val mul : positive -> positive -> positive
-  
-  val iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1
-  
-  val pow : positive -> positive -> positive
-  
-  val div2 : positive -> positive
-  
-  val div2_up : positive -> positive
-  
-  val size_nat : positive -> nat
-  
-  val size : positive -> positive
-  
-  val compare_cont : positive -> positive -> comparison -> comparison
-  
-  val compare : positive -> positive -> comparison
-  
-  val min : positive -> positive -> positive
-  
-  val max : positive -> positive -> positive
-  
-  val eqb : positive -> positive -> bool
-  
-  val leb : positive -> positive -> bool
-  
-  val ltb : positive -> positive -> bool
-  
-  val sqrtrem_step :
-    (positive -> positive) -> (positive -> positive) -> (positive * mask) ->
-    positive * mask
-  
-  val sqrtrem : positive -> positive * mask
-  
-  val sqrt : positive -> positive
-  
-  val gcdn : nat -> positive -> positive -> positive
-  
-  val gcd : positive -> positive -> positive
-  
-  val ggcdn : nat -> positive -> positive -> positive * (positive * positive)
-  
-  val ggcd : positive -> positive -> positive * (positive * positive)
-  
-  val coq_Nsucc_double : n -> n
-  
-  val coq_Ndouble : n -> n
-  
-  val coq_lor : positive -> positive -> positive
-  
-  val coq_land : positive -> positive -> n
-  
-  val ldiff : positive -> positive -> n
-  
-  val coq_lxor : positive -> positive -> n
-  
-  val shiftl_nat : positive -> nat -> positive
-  
-  val shiftr_nat : positive -> nat -> positive
-  
-  val shiftl : positive -> n -> positive
-  
-  val shiftr : positive -> n -> positive
-  
-  val testbit_nat : positive -> nat -> bool
-  
-  val testbit : positive -> n -> bool
-  
-  val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1
-  
-  val to_nat : positive -> nat
-  
-  val of_nat : nat -> positive
-  
-  val of_succ_nat : nat -> positive
  end
 
-module Coq_Pos : 
- sig 
-  module Coq__1 : sig 
-   type t = positive
-  end
-  type t = Coq__1.t
-  
+module Coq_Pos :
+ sig
   val succ : positive -> positive
-  
+
   val add : positive -> positive -> positive
-  
+
   val add_carry : positive -> positive -> positive
-  
+
   val pred_double : positive -> positive
-  
-  val pred : positive -> positive
-  
-  val pred_N : positive -> n
-  
+
   type mask = Pos.mask =
   | IsNul
   | IsPos of positive
   | IsNeg
-  
-  val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1
-  
-  val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1
-  
+
   val succ_double_mask : mask -> mask
-  
+
   val double_mask : mask -> mask
-  
+
   val double_pred_mask : positive -> mask
-  
-  val pred_mask : mask -> mask
-  
+
   val sub_mask : positive -> positive -> mask
-  
+
   val sub_mask_carry : positive -> positive -> mask
-  
+
   val sub : positive -> positive -> positive
-  
+
   val mul : positive -> positive -> positive
-  
-  val iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1
-  
-  val pow : positive -> positive -> positive
-  
-  val div2 : positive -> positive
-  
-  val div2_up : positive -> positive
-  
+
   val size_nat : positive -> nat
-  
-  val size : positive -> positive
-  
-  val compare_cont : positive -> positive -> comparison -> comparison
-  
+
+  val compare_cont : comparison -> positive -> positive -> comparison
+
   val compare : positive -> positive -> comparison
-  
-  val min : positive -> positive -> positive
-  
-  val max : positive -> positive -> positive
-  
-  val eqb : positive -> positive -> bool
-  
-  val leb : positive -> positive -> bool
-  
-  val ltb : positive -> positive -> bool
-  
-  val sqrtrem_step :
-    (positive -> positive) -> (positive -> positive) -> (positive * mask) ->
-    positive * mask
-  
-  val sqrtrem : positive -> positive * mask
-  
-  val sqrt : positive -> positive
-  
+
   val gcdn : nat -> positive -> positive -> positive
-  
+
   val gcd : positive -> positive -> positive
-  
-  val ggcdn : nat -> positive -> positive -> positive * (positive * positive)
-  
-  val ggcd : positive -> positive -> positive * (positive * positive)
-  
-  val coq_Nsucc_double : n -> n
-  
-  val coq_Ndouble : n -> n
-  
-  val coq_lor : positive -> positive -> positive
-  
-  val coq_land : positive -> positive -> n
-  
-  val ldiff : positive -> positive -> n
-  
-  val coq_lxor : positive -> positive -> n
-  
-  val shiftl_nat : positive -> nat -> positive
-  
-  val shiftr_nat : positive -> nat -> positive
-  
-  val shiftl : positive -> n -> positive
-  
-  val shiftr : positive -> n -> positive
-  
-  val testbit_nat : positive -> nat -> bool
-  
-  val testbit : positive -> n -> bool
-  
-  val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1
-  
-  val to_nat : positive -> nat
-  
-  val of_nat : nat -> positive
-  
+
   val of_succ_nat : nat -> positive
-  
-  val eq_dec : positive -> positive -> bool
-  
-  val peano_rect : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1
-  
-  val peano_rec : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1
-  
-  type coq_PeanoView =
-  | PeanoOne
-  | PeanoSucc of positive * coq_PeanoView
-  
-  val coq_PeanoView_rect :
-    'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive ->
-    coq_PeanoView -> 'a1
-  
-  val coq_PeanoView_rec :
-    'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive ->
-    coq_PeanoView -> 'a1
-  
-  val peanoView_xO : positive -> coq_PeanoView -> coq_PeanoView
-  
-  val peanoView_xI : positive -> coq_PeanoView -> coq_PeanoView
-  
-  val peanoView : positive -> coq_PeanoView
-  
-  val coq_PeanoView_iter :
-    'a1 -> (positive -> 'a1 -> 'a1) -> positive -> coq_PeanoView -> 'a1
-  
-  val switch_Eq : comparison -> comparison -> comparison
-  
-  val mask2cmp : mask -> comparison
-  
-  module T : 
-   sig 
-    
-   end
-  
-  module ORev : 
-   sig 
-    type t = Coq__1.t
-   end
-  
-  module MRev : 
-   sig 
-    val max : t -> t -> t
-   end
-  
-  module MPRev : 
-   sig 
-    module T : 
-     sig 
-      
-     end
-   end
-  
-  module P : 
-   sig 
-    val max_case_strong :
-      t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
-      'a1
-    
-    val max_case :
-      t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1
-    
-    val max_dec : t -> t -> bool
-    
-    val min_case_strong :
-      t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
-      'a1
-    
-    val min_case :
-      t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1
-    
-    val min_dec : t -> t -> bool
-   end
-  
-  val max_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
-  
-  val max_case : t -> t -> 'a1 -> 'a1 -> 'a1
-  
-  val max_dec : t -> t -> bool
-  
-  val min_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
-  
-  val min_case : t -> t -> 'a1 -> 'a1 -> 'a1
-  
-  val min_dec : t -> t -> bool
  end
 
-module N : 
- sig 
-  type t = n
-  
-  val zero : n
-  
-  val one : n
-  
-  val two : n
-  
-  val succ_double : n -> n
-  
-  val double : n -> n
-  
-  val succ : n -> n
-  
-  val pred : n -> n
-  
-  val succ_pos : n -> positive
-  
-  val add : n -> n -> n
-  
-  val sub : n -> n -> n
-  
-  val mul : n -> n -> n
-  
-  val compare : n -> n -> comparison
-  
-  val eqb : n -> n -> bool
-  
-  val leb : n -> n -> bool
-  
-  val ltb : n -> n -> bool
-  
-  val min : n -> n -> n
-  
-  val max : n -> n -> n
-  
-  val div2 : n -> n
-  
-  val even : n -> bool
-  
-  val odd : n -> bool
-  
-  val pow : n -> n -> n
-  
-  val log2 : n -> n
-  
-  val size : n -> n
-  
-  val size_nat : n -> nat
-  
-  val pos_div_eucl : positive -> n -> n * n
-  
-  val div_eucl : n -> n -> n * n
-  
-  val div : n -> n -> n
-  
-  val modulo : n -> n -> n
-  
-  val gcd : n -> n -> n
-  
-  val ggcd : n -> n -> n * (n * n)
-  
-  val sqrtrem : n -> n * n
-  
-  val sqrt : n -> n
-  
-  val coq_lor : n -> n -> n
-  
-  val coq_land : n -> n -> n
-  
-  val ldiff : n -> n -> n
-  
-  val coq_lxor : n -> n -> n
-  
-  val shiftl_nat : n -> nat -> n
-  
-  val shiftr_nat : n -> nat -> n
-  
-  val shiftl : n -> n -> n
-  
-  val shiftr : n -> n -> n
-  
-  val testbit_nat : n -> nat -> bool
-  
-  val testbit : n -> n -> bool
-  
-  val to_nat : n -> nat
-  
+module N :
+ sig
   val of_nat : nat -> n
-  
-  val iter : n -> ('a1 -> 'a1) -> 'a1 -> 'a1
-  
-  val eq_dec : n -> n -> bool
-  
-  val discr : n -> positive option
-  
-  val binary_rect : 'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1
-  
-  val binary_rec : 'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1
-  
-  val peano_rect : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1
-  
-  val peano_rec : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1
-  
-  module BootStrap : 
-   sig 
-    
-   end
-  
-  val recursion : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1
-  
-  module OrderElts : 
-   sig 
-    type t = n
-   end
-  
-  module OrderTac : 
-   sig 
-    
-   end
-  
-  module NZPowP : 
-   sig 
-    
-   end
-  
-  module NZSqrtP : 
-   sig 
-    
-   end
-  
-  val sqrt_up : n -> n
-  
-  val log2_up : n -> n
-  
-  module NZDivP : 
-   sig 
-    
-   end
-  
-  val lcm : n -> n -> n
-  
-  val b2n : bool -> n
-  
-  val setbit : n -> n -> n
-  
-  val clearbit : n -> n -> n
-  
-  val ones : n -> n
-  
-  val lnot : n -> n -> n
-  
-  module T : 
-   sig 
-    
-   end
-  
-  module ORev : 
-   sig 
-    type t = n
-   end
-  
-  module MRev : 
-   sig 
-    val max : n -> n -> n
-   end
-  
-  module MPRev : 
-   sig 
-    module T : 
-     sig 
-      
-     end
-   end
-  
-  module P : 
-   sig 
-    val max_case_strong :
-      n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
-      'a1
-    
-    val max_case :
-      n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1
-    
-    val max_dec : n -> n -> bool
-    
-    val min_case_strong :
-      n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
-      'a1
-    
-    val min_case :
-      n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1
-    
-    val min_dec : n -> n -> bool
-   end
-  
-  val max_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
-  
-  val max_case : n -> n -> 'a1 -> 'a1 -> 'a1
-  
-  val max_dec : n -> n -> bool
-  
-  val min_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
-  
-  val min_case : n -> n -> 'a1 -> 'a1 -> 'a1
-  
-  val min_dec : n -> n -> bool
  end
 
 val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1
@@ -616,225 +92,45 @@ val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
 
 val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1
 
-module Z : 
- sig 
-  type t = z
-  
-  val zero : z
-  
-  val one : z
-  
-  val two : z
-  
+module Z :
+ sig
   val double : z -> z
-  
+
   val succ_double : z -> z
-  
+
   val pred_double : z -> z
-  
+
   val pos_sub : positive -> positive -> z
-  
+
   val add : z -> z -> z
-  
+
   val opp : z -> z
-  
-  val succ : z -> z
-  
-  val pred : z -> z
-  
+
   val sub : z -> z -> z
-  
+
   val mul : z -> z -> z
-  
-  val pow_pos : z -> positive -> z
-  
-  val pow : z -> z -> z
-  
+
   val compare : z -> z -> comparison
-  
-  val sgn : z -> z
-  
+
   val leb : z -> z -> bool
-  
-  val geb : z -> z -> bool
-  
+
   val ltb : z -> z -> bool
-  
+
   val gtb : z -> z -> bool
-  
-  val eqb : z -> z -> bool
-  
+
   val max : z -> z -> z
-  
-  val min : z -> z -> z
-  
+
   val abs : z -> z
-  
-  val abs_nat : z -> nat
-  
-  val abs_N : z -> n
-  
-  val to_nat : z -> nat
-  
+
   val to_N : z -> n
-  
-  val of_nat : nat -> z
-  
-  val of_N : n -> z
-  
-  val iter : z -> ('a1 -> 'a1) -> 'a1 -> 'a1
-  
+
   val pos_div_eucl : positive -> z -> z * z
-  
+
   val div_eucl : z -> z -> z * z
-  
+
   val div : z -> z -> z
-  
-  val modulo : z -> z -> z
-  
-  val quotrem : z -> z -> z * z
-  
-  val quot : z -> z -> z
-  
-  val rem : z -> z -> z
-  
-  val even : z -> bool
-  
-  val odd : z -> bool
-  
-  val div2 : z -> z
-  
-  val quot2 : z -> z
-  
-  val log2 : z -> z
-  
-  val sqrtrem : z -> z * z
-  
-  val sqrt : z -> z
-  
+
   val gcd : z -> z -> z
-  
-  val ggcd : z -> z -> z * (z * z)
-  
-  val testbit : z -> z -> bool
-  
-  val shiftl : z -> z -> z
-  
-  val shiftr : z -> z -> z
-  
-  val coq_lor : z -> z -> z
-  
-  val coq_land : z -> z -> z
-  
-  val ldiff : z -> z -> z
-  
-  val coq_lxor : z -> z -> z
-  
-  val eq_dec : z -> z -> bool
-  
-  module BootStrap : 
-   sig 
-    
-   end
-  
-  module OrderElts : 
-   sig 
-    type t = z
-   end
-  
-  module OrderTac : 
-   sig 
-    
-   end
-  
-  val sqrt_up : z -> z
-  
-  val log2_up : z -> z
-  
-  module NZDivP : 
-   sig 
-    
-   end
-  
-  module Quot2Div : 
-   sig 
-    val div : z -> z -> z
-    
-    val modulo : z -> z -> z
-   end
-  
-  module NZQuot : 
-   sig 
-    
-   end
-  
-  val lcm : z -> z -> z
-  
-  val b2z : bool -> z
-  
-  val setbit : z -> z -> z
-  
-  val clearbit : z -> z -> z
-  
-  val lnot : z -> z
-  
-  val ones : z -> z
-  
-  module T : 
-   sig 
-    
-   end
-  
-  module ORev : 
-   sig 
-    type t = z
-   end
-  
-  module MRev : 
-   sig 
-    val max : z -> z -> z
-   end
-  
-  module MPRev : 
-   sig 
-    module T : 
-     sig 
-      
-     end
-   end
-  
-  module P : 
-   sig 
-    val max_case_strong :
-      z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
-      'a1
-    
-    val max_case :
-      z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1
-    
-    val max_dec : z -> z -> bool
-    
-    val min_case_strong :
-      z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
-      'a1
-    
-    val min_case :
-      z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1
-    
-    val min_dec : z -> z -> bool
-   end
-  
-  val max_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
-  
-  val max_case : z -> z -> 'a1 -> 'a1 -> 'a1
-  
-  val max_dec : z -> z -> bool
-  
-  val min_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
-  
-  val min_case : z -> z -> 'a1 -> 'a1 -> 'a1
-  
-  val min_dec : z -> z -> bool
  end
 
 val zeq_bool : z -> z -> bool
@@ -872,44 +168,44 @@ val paddI :
   positive -> 'a1 pol -> 'a1 pol
 
 val psubI :
-  ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) ->
-  'a1 pol -> positive -> 'a1 pol -> 'a1 pol
+  ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol)
+  -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
 
 val paddX :
-  'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol
-  -> positive -> 'a1 pol -> 'a1 pol
+  'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1
+  pol -> positive -> 'a1 pol -> 'a1 pol
 
 val psubX :
-  'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1
-  pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
+  'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol ->
+  'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
 
 val padd :
-  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol ->
-  'a1 pol
+  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol
+  -> 'a1 pol
 
 val psub :
-  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
-  -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
+  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) ->
+  ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
 
 val pmulC_aux :
-  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1
-  pol
+  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 ->
+  'a1 pol
 
 val pmulC :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1
-  -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol ->
+  'a1 -> 'a1 pol
 
 val pmulI :
   'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol ->
   'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
 
 val pmul :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
 
 val psquare :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  bool) -> 'a1 pol -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> bool) -> 'a1 pol -> 'a1 pol
 
 type 'c pExpr =
 | PEc of 'c
@@ -923,16 +219,17 @@ type 'c pExpr =
 val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol
 
 val ppow_pos :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive ->
+  'a1 pol
 
 val ppow_N :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol
 
 val norm_aux :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
 
 type 'a bFormula =
 | TT
@@ -946,9 +243,9 @@ type 'a bFormula =
 
 val map_bformula : ('a1 -> 'a2) -> 'a1 bFormula -> 'a2 bFormula
 
-type 'term' clause = 'term' list
+type 'x clause = 'x list
 
-type 'term' cnf = 'term' clause list
+type 'x cnf = 'x clause list
 
 val tt : 'a1 cnf
 
@@ -959,12 +256,12 @@ val add_term :
   clause option
 
 val or_clause :
-  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 clause ->
-  'a1 clause option
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 clause
+  -> 'a1 clause option
 
 val or_clause_cnf :
-  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf -> 'a1
-  cnf
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf ->
+  'a1 cnf
 
 val or_cnf :
   ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> 'a1
@@ -973,18 +270,20 @@ val or_cnf :
 val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf
 
 val xcnf :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 ->
-  'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1
+  -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf
 
 val cnf_checker : ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool
 
 val tauto_checker :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 ->
-  'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 list -> bool
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1
+  -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 list ->
+  bool
 
 val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
 
-val cltb : ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
+val cltb :
+  ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
 
 type 'c polC = 'c pol
 
@@ -1015,28 +314,30 @@ val map_option2 :
   ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option
 
 val pexpr_times_nformula :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option
 
 val nformula_times_nformula :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option
 
 val nformula_plus_nformula :
-  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1
-  nFormula -> 'a1 nFormula option
+  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula ->
+  'a1 nFormula -> 'a1 nFormula option
 
 val eval_Psatz :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1
-  nFormula option
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz ->
+  'a1 nFormula option
 
 val check_inconsistent :
-  'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool
+  'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula ->
+  bool
 
 val check_normalised_formulas :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz ->
+  bool
 
 type op2 =
 | OpEq
@@ -1048,43 +349,37 @@ type op2 =
 
 type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr }
 
-val flhs : 'a1 formula -> 'a1 pExpr
-
-val fop : 'a1 formula -> op2
-
-val frhs : 'a1 formula -> 'a1 pExpr
-
 val norm :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
 
 val psub0 :
-  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
-  -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
+  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) ->
+  ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
 
 val padd0 :
-  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol ->
-  'a1 pol
+  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol
+  -> 'a1 pol
 
 val xnormalise :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
-  list
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1
+  nFormula list
 
 val cnf_normalise :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
-  cnf
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1
+  nFormula cnf
 
 val xnegate :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
-  list
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1
+  nFormula list
 
 val cnf_negate :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
-  'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
-  cnf
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+  -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1
+  nFormula cnf
 
 val xdenorm : positive -> 'a1 pol -> 'a1 pExpr
 
@@ -1095,8 +390,8 @@ val map_PExpr : ('a2 -> 'a1) -> 'a2 pExpr -> 'a1 pExpr
 val map_Formula : ('a2 -> 'a1) -> 'a2 formula -> 'a1 formula
 
 val simpl_cone :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz ->
-  'a1 psatz
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz
+  -> 'a1 psatz
 
 type q = { qnum : z; qden : positive }
 
@@ -1122,12 +417,16 @@ val qpower_positive : q -> positive -> q
 
 val qpower : q -> z -> q
 
-type 'a t0 =
+type 'a t =
 | Empty
 | Leaf of 'a
-| Node of 'a t0 * 'a * 'a t0
+| Node of 'a t * 'a * 'a t
+
+val find : 'a1 -> 'a1 t -> positive -> 'a1
 
-val find : 'a1 -> 'a1 t0 -> positive -> 'a1
+val singleton : 'a1 -> positive -> 'a1 -> 'a1 t
+
+val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t
 
 type zWitness = z psatz
 
@@ -1221,4 +520,3 @@ val runsat : q nFormula -> bool
 val rdeduce : q nFormula -> q nFormula -> q nFormula option
 
 val rTautoChecker : rcst formula bFormula -> rWitness list -> bool
-
diff --git a/plugins/micromega/vo.itarget b/plugins/micromega/vo.itarget
index cb4b2b8a5..c9009ea4d 100644
--- a/plugins/micromega/vo.itarget
+++ b/plugins/micromega/vo.itarget
@@ -12,4 +12,4 @@ ZCoeff.vo
 ZMicromega.vo
 Lia.vo
 Lqa.vo
-Lra.vo
\ No newline at end of file
+Lra.vo
diff --git a/test-suite/micromega/bertot.v b/test-suite/micromega/bertot.v
index bcf222f92..29171aed9 100644
--- a/test-suite/micromega/bertot.v
+++ b/test-suite/micromega/bertot.v
@@ -11,6 +11,8 @@ Require Import Psatz.
 
 Open Scope Z_scope.
 
+
+
 Goal (forall x y n,
   ( ~ x < n /\ x <= n /\ 2 * y = x*(x+1) -> 2 * y = n*(n+1))
   /\
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 89c08c770..12f72a580 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -11,6 +11,12 @@ Require Import Reals.
 
 Open Scope R_scope.
 
+
+Lemma cst_test : 5^5 = 5 * 5 * 5 *5 *5.
+Proof.
+  lra.
+Qed.
+
 Lemma yplus_minus : forall x y,
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
@@ -73,4 +79,5 @@ Qed.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
 intros; split_Rabs; lra.
-Qed.
\ No newline at end of file
+Qed.
+
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 1f148becc..3f4c2407d 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -8,9 +8,10 @@ Proof.
   lia.
 Qed.
 
+
 Lemma two_x_y_eq_1 : forall x y, 2 * x + 2 * y = 1 -> False.
 Proof.
-  intros.
+  intros. 
   lia.
 Qed.
 
@@ -20,6 +21,12 @@ Proof.
   lia.
 Qed.
 
+Lemma unused : forall x y, y >= 0 /\ x = 1 -> x = 1.
+Proof.
+  intros x y.
+  lia.
+Qed.
+
 Lemma omega_nightmare : forall x y, 27 <= 11 * x + 13 * y <= 45 ->  -10 <= 7 * x - 9 * y <= 4 -> False.
 Proof.
   intros ; intuition auto.
@@ -42,4 +49,37 @@ Proof.
   Unshelve.
   exact Z0.
 Qed.
-  
\ No newline at end of file
+
+Lemma unused_concl : forall x,
+    False -> x > 0 -> x < 0.
+Proof.
+  intro.
+  lia.
+Qed.
+
+Lemma unused_concl_match : forall (x:Z),
+    False -> match x with
+             | Z0 => True
+             | _ => x = x
+             end.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Lemma fresh : forall (__arith : Prop),
+    __arith -> True.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Class Foo {x : Z} := { T : Type ; dec : T -> Z }.
+Goal forall bound {F : @Foo bound} (x y : T), 0 <= dec x < bound -> 0 <= dec y 
+< bound -> dec x + dec y >= bound -> dec x + dec y < 2 * bound.
+Proof.
+  intros.
+  lia.
+Qed.
+
+