Merge remote-tracking branch 'upstream/trunk' into trunk

5 files changed, 2494 insertions, 168 deletions

diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 4d5c3b1d5b..2451aeada7 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -48,7 +48,7 @@ Extract Constant Rmult => "( * )".
 Extract Constant Ropp  => "fun x -> - x".
 Extract Constant Rinv   => "fun x -> 1 / x".
 
-Extraction "plugins/micromega/micromega.ml"
+Extraction "plugins/micromega/generated_micromega.ml"
   List.map simpl_cone (*map_cone  indexes*)
   denorm Qpower vm_add
   n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 03041ea0ab..fba1966df3 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -20,8 +20,7 @@ open API
 open Pp
 open Mutils
 open Goptions
-
-module Term = EConstr
+open Names
 
 (**
   * Debug flag 
@@ -110,8 +109,8 @@ type 'cst atom = 'cst Micromega.formula
 type 'cst formula =
   | TT
   | FF
-  | X of Term.constr
-  | A of 'cst atom * tag * Term.constr
+  | X of EConstr.constr
+  | A of 'cst atom * tag * EConstr.constr
   | C of 'cst formula * 'cst formula
   | D of 'cst formula * 'cst formula
   | N of 'cst formula
@@ -329,9 +328,6 @@ let selecti s m =
 module M =
 struct
 
-  open Constr
-  open EConstr
-
   (**
     * Location of the Coq libraries.
     *)
@@ -603,10 +599,10 @@ struct
 
   let get_left_construct sigma term =
    match EConstr.kind sigma term with
-    | Constr.Construct((_,i),_) -> (i,[| |])
-    | Constr.App(l,rst) ->
+    | Term.Construct((_,i),_) -> (i,[| |])
+    | Term.App(l,rst) ->
        (match EConstr.kind sigma l with
-        | Constr.Construct((_,i),_) -> (i,rst)
+        | Term.Construct((_,i),_) -> (i,rst)
         |   _     -> raise ParseError
        )
     | _ ->   raise ParseError
@@ -627,7 +623,7 @@ struct
   let rec dump_nat x =
    match x with
     | Mc.O -> Lazy.force coq_O
-    | Mc.S p -> Term.mkApp(Lazy.force coq_S,[| dump_nat p |])
+    | Mc.S p -> EConstr.mkApp(Lazy.force coq_S,[| dump_nat p |])
 
   let rec parse_positive sigma term =
    let (i,c) = get_left_construct sigma term in
@@ -640,28 +636,28 @@ struct
   let rec dump_positive x =
    match x with
     | Mc.XH -> Lazy.force coq_xH
-    | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_positive p |])
-    | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_positive p |])
+    | Mc.XO p -> EConstr.mkApp(Lazy.force coq_xO,[| dump_positive p |])
+    | Mc.XI p -> EConstr.mkApp(Lazy.force coq_xI,[| dump_positive p |])
 
   let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x)
 
   let dump_n x =
    match x with
     | Mc.N0 -> Lazy.force coq_N0
-    | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p|])
+    | Mc.Npos p -> EConstr.mkApp(Lazy.force coq_Npos,[| dump_positive p|])
 
   let rec dump_index x =
    match x with
     | Mc.XH -> Lazy.force coq_xH
-    | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_index p |])
-    | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_index p |])
+    | Mc.XO p -> EConstr.mkApp(Lazy.force coq_xO,[| dump_index p |])
+    | Mc.XI p -> EConstr.mkApp(Lazy.force coq_xI,[| dump_index p |])
 
   let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x)
 
   let pp_n o x =  output_string o  (string_of_int (CoqToCaml.n x))
 
   let dump_pair t1 t2 dump_t1 dump_t2 (x,y) =
-   Term.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|])
+   EConstr.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|])
 
   let parse_z sigma term =
    let (i,c) = get_left_construct sigma term in
@@ -674,23 +670,23 @@ struct
   let dump_z x =
    match x with
     | Mc.Z0 ->Lazy.force coq_ZERO
-    | Mc.Zpos p -> Term.mkApp(Lazy.force coq_POS,[| dump_positive p|])
-    | Mc.Zneg p -> Term.mkApp(Lazy.force coq_NEG,[| dump_positive p|])
+    | Mc.Zpos p -> EConstr.mkApp(Lazy.force coq_POS,[| dump_positive p|])
+    | Mc.Zneg p -> EConstr.mkApp(Lazy.force coq_NEG,[| dump_positive p|])
 
   let pp_z o x = Printf.fprintf o "%s" (Big_int.string_of_big_int (CoqToCaml.z_big_int x))
 
   let dump_num bd1 =
-   Term.mkApp(Lazy.force coq_Qmake,
-             [|dump_z (CamlToCoq.bigint (numerator bd1)) ;
-               dump_positive (CamlToCoq.positive_big_int (denominator bd1)) |])
+   EConstr.mkApp(Lazy.force coq_Qmake,
+                 [|dump_z (CamlToCoq.bigint (numerator bd1)) ;
+                   dump_positive (CamlToCoq.positive_big_int (denominator bd1)) |])
 
   let dump_q q =
-   Term.mkApp(Lazy.force coq_Qmake,
-             [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|])
+   EConstr.mkApp(Lazy.force coq_Qmake,
+                 [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|])
 
   let parse_q sigma term =
      match EConstr.kind sigma term with
-       | Constr.App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then
+       | Term.App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then
              {Mc.qnum = parse_z sigma args.(0) ; Mc.qden = parse_positive sigma args.(1) }
        else raise ParseError
    |  _ -> raise ParseError
@@ -713,13 +709,13 @@ struct
     match cst with
       | Mc.C0 -> Lazy.force coq_C0 
       | Mc.C1 ->  Lazy.force coq_C1
-      | Mc.CQ q ->  Term.mkApp(Lazy.force coq_CQ, [| dump_q q |])
-      | Mc.CZ z -> Term.mkApp(Lazy.force coq_CZ, [| dump_z z |])
-      | Mc.CPlus(x,y) -> Term.mkApp(Lazy.force coq_CPlus, [| dump_Rcst x ; dump_Rcst y |])
-      | Mc.CMinus(x,y) -> Term.mkApp(Lazy.force coq_CMinus, [| dump_Rcst x ; dump_Rcst y |])
-      | Mc.CMult(x,y) -> Term.mkApp(Lazy.force coq_CMult, [| dump_Rcst x ; dump_Rcst y |])
-      | Mc.CInv t -> Term.mkApp(Lazy.force coq_CInv, [| dump_Rcst t |])
-      | Mc.COpp t -> Term.mkApp(Lazy.force coq_COpp, [| dump_Rcst t |])
+      | Mc.CQ q ->  EConstr.mkApp(Lazy.force coq_CQ, [| dump_q q |])
+      | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_CZ, [| dump_z z |])
+      | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_CPlus, [| dump_Rcst x ; dump_Rcst y |])
+      | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_CMinus, [| dump_Rcst x ; dump_Rcst y |])
+      | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_CMult, [| dump_Rcst x ; dump_Rcst y |])
+      | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_CInv, [| dump_Rcst t |])
+      | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_COpp, [| dump_Rcst t |])
 
   let rec parse_Rcst sigma term = 
     let (i,c) = get_left_construct sigma term in
@@ -746,8 +742,8 @@ struct
 
   let rec dump_list typ dump_elt l =
    match l with
-    | [] -> Term.mkApp(Lazy.force coq_nil,[| typ |])
-    | e :: l -> Term.mkApp(Lazy.force coq_cons,
+    | [] -> EConstr.mkApp(Lazy.force coq_nil,[| typ |])
+    | e :: l -> EConstr.mkApp(Lazy.force coq_cons,
                                 [| typ; dump_elt e;dump_list typ dump_elt l|])
 
   let pp_list op cl elt o l =
@@ -777,27 +773,27 @@ struct
   let dump_expr typ dump_z e =
    let rec dump_expr  e =
    match e with
-    | Mc.PEX n -> mkApp(Lazy.force coq_PEX,[| typ; dump_var n |])
-    | Mc.PEc z -> mkApp(Lazy.force coq_PEc,[| typ ; dump_z z |])
-    | Mc.PEadd(e1,e2) -> mkApp(Lazy.force coq_PEadd,
-                              [| typ; dump_expr e1;dump_expr e2|])
-    | Mc.PEsub(e1,e2) -> mkApp(Lazy.force coq_PEsub,
-                              [| typ; dump_expr  e1;dump_expr  e2|])
-    | Mc.PEopp e -> mkApp(Lazy.force coq_PEopp,
-                         [| typ; dump_expr  e|])
-    | Mc.PEmul(e1,e2) ->  mkApp(Lazy.force coq_PEmul,
-                               [| typ; dump_expr  e1;dump_expr e2|])
-    | Mc.PEpow(e,n) ->  mkApp(Lazy.force coq_PEpow,
-                             [| typ; dump_expr  e; dump_n  n|])
+    | Mc.PEX n -> EConstr.mkApp(Lazy.force coq_PEX,[| typ; dump_var n |])
+    | Mc.PEc z -> EConstr.mkApp(Lazy.force coq_PEc,[| typ ; dump_z z |])
+    | Mc.PEadd(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEadd,
+                                       [| typ; dump_expr e1;dump_expr e2|])
+    | Mc.PEsub(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEsub,
+                                       [| typ; dump_expr  e1;dump_expr  e2|])
+    | Mc.PEopp e -> EConstr.mkApp(Lazy.force coq_PEopp,
+                                  [| typ; dump_expr  e|])
+    | Mc.PEmul(e1,e2) ->  EConstr.mkApp(Lazy.force coq_PEmul,
+                                        [| typ; dump_expr  e1;dump_expr e2|])
+    | Mc.PEpow(e,n) ->  EConstr.mkApp(Lazy.force coq_PEpow,
+                                      [| typ; dump_expr  e; dump_n  n|])
       in
     dump_expr e
 
   let dump_pol typ dump_c e =
     let rec dump_pol e =
       match e with
-        | Mc.Pc n -> mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|])
-        | Mc.Pinj(p,pol) -> mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|])
-        | Mc.PX(pol1,p,pol2) -> mkApp(Lazy.force coq_PX, [| typ ; dump_pol pol1 ; dump_positive p ; dump_pol pol2|]) in
+        | Mc.Pc n -> EConstr.mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|])
+        | Mc.Pinj(p,pol) -> EConstr.mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|])
+        | Mc.PX(pol1,p,pol2) -> EConstr.mkApp(Lazy.force coq_PX, [| typ ; dump_pol pol1 ; dump_positive p ; dump_pol pol2|]) in
       dump_pol e
 
   let pp_pol pp_c o e =
@@ -816,17 +812,17 @@ struct
    let z = Lazy.force typ in
   let rec dump_cone e =
    match e with
-    | Mc.PsatzIn n -> mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |])
-    | Mc.PsatzMulC(e,c) -> mkApp(Lazy.force coq_PsatzMultC,
-                              [| z; dump_pol z dump_z e ; dump_cone c |])
-    | Mc.PsatzSquare e -> mkApp(Lazy.force coq_PsatzSquare,
-                            [| z;dump_pol z dump_z e|])
-    | Mc.PsatzAdd(e1,e2) -> mkApp(Lazy.force coq_PsatzAdd,
-                              [| z; dump_cone e1; dump_cone e2|])
-    | Mc.PsatzMulE(e1,e2) -> mkApp(Lazy.force coq_PsatzMulE,
-                               [| z; dump_cone e1; dump_cone e2|])
-    | Mc.PsatzC p -> mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|])
-    | Mc.PsatzZ    -> mkApp( Lazy.force coq_PsatzZ,[| z|]) in
+    | Mc.PsatzIn n -> EConstr.mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |])
+    | Mc.PsatzMulC(e,c) -> EConstr.mkApp(Lazy.force coq_PsatzMultC,
+                                         [| z; dump_pol z dump_z e ; dump_cone c |])
+    | Mc.PsatzSquare e -> EConstr.mkApp(Lazy.force coq_PsatzSquare,
+                                        [| z;dump_pol z dump_z e|])
+    | Mc.PsatzAdd(e1,e2) -> EConstr.mkApp(Lazy.force coq_PsatzAdd,
+                                          [| z; dump_cone e1; dump_cone e2|])
+    | Mc.PsatzMulE(e1,e2) -> EConstr.mkApp(Lazy.force coq_PsatzMulE,
+                                           [| z; dump_cone e1; dump_cone e2|])
+    | Mc.PsatzC p -> EConstr.mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|])
+    | Mc.PsatzZ    -> EConstr.mkApp(Lazy.force coq_PsatzZ,[| z|]) in
    dump_cone e
 
   let  pp_psatz pp_z o e =
@@ -869,10 +865,10 @@ struct
    Printf.fprintf o"(%a %a %a)" (pp_expr pp_z) l pp_op op (pp_expr pp_z) r
 
   let dump_cstr typ dump_constant {Mc.flhs = e1 ; Mc.fop = o ; Mc.frhs = e2} =
-    Term.mkApp(Lazy.force coq_Build,
-              [| typ; dump_expr typ dump_constant e1 ;
-                 dump_op o ;
-                 dump_expr typ dump_constant e2|])
+    EConstr.mkApp(Lazy.force coq_Build,
+                  [| typ; dump_expr typ dump_constant e1 ;
+                     dump_op o ;
+                     dump_expr typ dump_constant e2|])
 
   let assoc_const sigma x l =
    try
@@ -906,8 +902,8 @@ struct
   let parse_zop gl (op,args) =
     let sigma = gl.sigma in
     match EConstr.kind sigma op with
-    | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1))
-    | Ind((n,0),_) ->
+    | Term.Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1))
+    | Term.Ind((n,0),_) ->
         if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z)
         then (Mc.OpEq, args.(1), args.(2))
         else raise ParseError
@@ -916,8 +912,8 @@ struct
   let parse_rop gl (op,args) =
     let sigma = gl.sigma in
     match EConstr.kind sigma op with
-     | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1))
-     | Ind((n,0),_) ->
+     | Term.Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1))
+     | Term.Ind((n,0),_) ->
         if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R)
         then (Mc.OpEq, args.(1), args.(2))
         else raise ParseError
@@ -928,7 +924,7 @@ struct
 
   let is_constant sigma t = (* This is an approx *)
    match EConstr.kind sigma t with
-    | Construct(i,_) -> true
+    | Term.Construct(i,_) -> true
     |   _ -> false
 
   type 'a op =
@@ -949,14 +945,14 @@ struct
 
   module Env =
   struct
-   type t = constr list
+   type t = EConstr.constr list
 
    let compute_rank_add env sigma v =
     let rec _add env n v =
      match env with
       | [] -> ([v],n)
       | e::l ->
-         if eq_constr sigma e v
+         if EConstr.eq_constr sigma e v
          then (env,n)
          else
           let (env,n) = _add l ( n+1) v in
@@ -970,7 +966,7 @@ struct
        match env with
        | [] -> raise (Invalid_argument "get_rank")
       | e::l ->
-         if eq_constr sigma e v
+         if EConstr.eq_constr sigma e v
          then n
          else  _get_rank l (n+1)  in 
      _get_rank env 1
@@ -1011,10 +1007,10 @@ struct
        try (Mc.PEc (parse_constant term) , env)
        with ParseError -> 
 	 match EConstr.kind sigma term with
-	   | App(t,args) ->
+	   | Term.App(t,args) ->
                (
 		 match EConstr.kind sigma t with
-		   | Const c ->
+		   | Term.Const c ->
 		       ( match assoc_ops sigma t ops_spec  with
 			   | Binop f -> combine env f (args.(0),args.(1))
                    | Opp     -> let (expr,env) = parse_expr env args.(0) in
@@ -1077,13 +1073,13 @@ struct
 
   let rec rconstant sigma term =
    match EConstr.kind sigma term with
-    | Const x ->
+    | Term.Const x ->
         if EConstr.eq_constr sigma term (Lazy.force coq_R0)
         then Mc.C0
         else if EConstr.eq_constr sigma term (Lazy.force coq_R1)
         then Mc.C1
         else raise ParseError
-    | App(op,args) -> 
+    | Term.App(op,args) -> 
 	begin
 	  try
             (* the evaluation order is important in the following *)
@@ -1152,7 +1148,7 @@ struct
    if debug
    then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ());
    match EConstr.kind sigma cstr with
-    | App(op,args) ->
+    | Term.App(op,args) ->
        let (op,lhs,rhs) = parse_op gl (op,args) in
        let (e1,env) = parse_expr sigma env lhs in
        let (e2,env) = parse_expr sigma env rhs in
@@ -1207,29 +1203,29 @@ struct
      
     let rec xparse_formula env tg term =
       match EConstr.kind sigma term with
-      | App(l,rst) ->
+      | Term.App(l,rst) ->
         (match rst with
-        | [|a;b|] when eq_constr sigma l (Lazy.force coq_and) ->
+        | [|a;b|] when EConstr.eq_constr sigma 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 sigma l (Lazy.force coq_or) ->
+        | [|a;b|] when EConstr.eq_constr sigma 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 sigma l (Lazy.force coq_not) ->
+        | [|a|] when EConstr.eq_constr sigma l (Lazy.force coq_not) ->
           let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg)
-        | [|a;b|] when eq_constr sigma l (Lazy.force coq_iff) ->
+        | [|a;b|] when EConstr.eq_constr sigma 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 Vars.noccurn sigma 1 b ->
+      | Term.Prod(typ,a,b) when EConstr.Vars.noccurn sigma 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 sigma term (Lazy.force coq_True) -> (TT,env,tg)
-      | _ when eq_constr sigma term (Lazy.force coq_False) -> (FF,env,tg)
+      | _ when EConstr.eq_constr sigma term (Lazy.force coq_True) -> (TT,env,tg)
+      | _ when EConstr.eq_constr sigma term (Lazy.force coq_False) -> (FF,env,tg)
       | _ when is_prop term -> X(term),env,tg
       | _ -> raise ParseError
     in
@@ -1238,14 +1234,14 @@ struct
   let dump_formula typ dump_atom f =
    let rec xdump f =
     match f with
-     | TT  -> mkApp(Lazy.force coq_TT,[|typ|])
-     | FF  -> mkApp(Lazy.force coq_FF,[|typ|])
-     | C(x,y) -> mkApp(Lazy.force coq_And,[|typ ; xdump x ; xdump y|])
-     | D(x,y) -> mkApp(Lazy.force coq_Or,[|typ ; xdump x ; xdump y|])
-     | I(x,_,y) -> mkApp(Lazy.force coq_Impl,[|typ ; xdump x ; xdump y|])
-     | N(x) -> mkApp(Lazy.force coq_Neg,[|typ ; xdump x|])
-     | A(x,_,_) -> mkApp(Lazy.force coq_Atom,[|typ ; dump_atom x|])
-     | X(t) -> mkApp(Lazy.force coq_X,[|typ ; t|])  in
+     | TT  -> EConstr.mkApp(Lazy.force coq_TT,[|typ|])
+     | FF  -> EConstr.mkApp(Lazy.force coq_FF,[|typ|])
+     | C(x,y) -> EConstr.mkApp(Lazy.force coq_And,[|typ ; xdump x ; xdump y|])
+     | D(x,y) -> EConstr.mkApp(Lazy.force coq_Or,[|typ ; xdump x ; xdump y|])
+     | I(x,_,y) -> EConstr.mkApp(Lazy.force coq_Impl,[|typ ; xdump x ; xdump y|])
+     | N(x) -> EConstr.mkApp(Lazy.force coq_Neg,[|typ ; xdump x|])
+     | A(x,_,_) -> EConstr.mkApp(Lazy.force coq_Atom,[|typ ; dump_atom x|])
+     | X(t) -> EConstr.mkApp(Lazy.force coq_X,[|typ ; t|])  in
    xdump f
 
 
@@ -1285,15 +1281,15 @@ struct
       
   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
+      interp_typ : EConstr.constr;
+      dump_cst : 'cst -> EConstr.constr;
+      dump_add : EConstr.constr;
+      dump_sub : EConstr.constr;
+      dump_opp : EConstr.constr;
+      dump_mul : EConstr.constr;
+      dump_pow : EConstr.constr;
+      dump_pow_arg : Mc.n -> EConstr.constr;
+      dump_op  : (Mc.op2 * EConstr.constr) list
     }
 
 let dump_zexpr = lazy
@@ -1327,8 +1323,8 @@ let dump_qexpr = lazy
   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 mk_add x y  = EConstr.mkApp(add,[|x;y|]) in
+  let mk_mult x y = EConstr.mkApp(mult,[|x;y|]) in
 
   let two  = mk_add one one in 
 
@@ -1351,13 +1347,13 @@ 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 |])
+  | Mc.CQ q ->  EConstr.mkApp(Lazy.force coq_IQR, [| dump_q q |])
+  | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_IZR, [| dump_z z |])
+  | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_Rplus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |])
+  | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_Rminus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |])
+  | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_Rmult, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |])
+  | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_Rinv, [| dump_Rcst_as_R t |])
+  | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_Ropp, [| dump_Rcst_as_R t |])
 
 
 let dump_rexpr = lazy
@@ -1386,7 +1382,7 @@ let dump_rexpr = lazy
 let prodn n env b =
   let rec prodrec = function
     | (0, env, b)        -> b
-    | (n, ((v,t)::l), b) -> prodrec (n-1,  l, mkProd (v,t,b))
+    | (n, ((v,t)::l), b) -> prodrec (n-1,  l, EConstr.mkProd (v,t,b))
     | _ -> assert false
   in
   prodrec (n,env,b)
@@ -1400,32 +1396,32 @@ let make_goal_of_formula sigma dexpr form =
   
   let props     = prop_env_of_formula sigma 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 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))) , EConstr.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.PEX n -> EConstr.mkRel (i+(List.assoc (CoqToCaml.positive n)  vars_idx))
     | Mc.PEc z -> dexpr.dump_cst z
-    | Mc.PEadd(e1,e2) -> mkApp(dexpr.dump_add,
+    | Mc.PEadd(e1,e2) -> EConstr.mkApp(dexpr.dump_add,
                                [| dump_expr e1;dump_expr e2|])
-    | Mc.PEsub(e1,e2) -> mkApp(dexpr.dump_sub,
+    | Mc.PEsub(e1,e2) -> EConstr.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|])
+    | Mc.PEopp e -> EConstr.mkApp(dexpr.dump_opp,
+                                  [| dump_expr  e|])
+    | Mc.PEmul(e1,e2) -> EConstr.mkApp(dexpr.dump_mul,
+                                       [| dump_expr  e1;dump_expr e2|])
+    | Mc.PEpow(e,n) -> EConstr.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|])
+        EConstr.mkApp(List.assoc op dexpr.dump_op, [| e1; e2|])
       with Not_found ->
-        Term.mkApp(Lazy.force coq_Eq,[|dexpr.interp_typ ; e1 ;e2|]) in
+        EConstr.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
@@ -1434,13 +1430,13 @@ let make_goal_of_formula sigma dexpr form =
     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)
+    | C(x,y) -> EConstr.mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|])
+    | D(x,y) -> EConstr.mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|])
+    | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y)
+    | N(x) -> EConstr.mkArrow (xdump pi xi x) (Lazy.force coq_False)
     | A(x,_,_) -> dump_cstr xi x
     | X(t) -> let idx = Env.get_rank props sigma t in
-              mkRel (pi+idx) in 
+              EConstr.mkRel (pi+idx) in 
   
   let nb_vars  = List.length vars_n  in
   let nb_props = List.length props_n in 
@@ -1449,12 +1445,12 @@ let make_goal_of_formula sigma dexpr form =
   
   let subst_prop p =
     let idx = Env.get_rank props sigma p in
-    mkVar (Names.id_of_string (Printf.sprintf "__p%i"  idx)) in 
+    EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i"  idx)) in 
 
   let form' = map_prop subst_prop   form in
 
-  (prodn nb_props (List.map (fun (x,y) -> Names.Name x,y) props_n)
-     (prodn nb_vars (List.map (fun (x,y) -> Names.Name x,y) vars_n)
+  (prodn nb_props (List.map (fun (x,y) -> Name.Name x,y) props_n)
+     (prodn nb_vars (List.map (fun (x,y) -> Name.Name x,y) vars_n)
         (xdump (List.length vars_n) 0  form)),
    List.rev props_n, List.rev var_name_pos,form')
     
@@ -1469,7 +1465,7 @@ let make_goal_of_formula sigma dexpr form =
     | [] -> acc
     | (e::l) ->
        let (name,expr,typ) = e in
-        xset (Term.mkNamedLetIn
+        xset (EConstr.mkNamedLetIn
                (Names.Id.of_string name)
                expr typ acc) l in
     xset concl l
@@ -1545,10 +1541,10 @@ let coq_VarMap =
 
 let rec dump_varmap typ m =
   match m with
-  | Mc.Empty -> Term.mkApp(Lazy.force coq_Empty,[| typ |])
-  | Mc.Leaf v -> Term.mkApp(Lazy.force coq_Leaf,[| typ; v|])
+  | Mc.Empty -> EConstr.mkApp(Lazy.force coq_Empty,[| typ |])
+  | Mc.Leaf v -> EConstr.mkApp(Lazy.force coq_Leaf,[| typ; v|])
   | Mc.Node(l,o,r) ->
-    Term.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
+    EConstr.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
 
 
 let vm_of_list env =
@@ -1570,15 +1566,15 @@ let rec pp_varmap o vm =
 let rec dump_proof_term = function
   | Micromega.DoneProof -> Lazy.force coq_doneProof
   | Micromega.RatProof(cone,rst) ->
-    Term.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|])
+    EConstr.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|])
  | Micromega.CutProof(cone,prf) ->
-    Term.mkApp(Lazy.force coq_cutProof,
+    EConstr.mkApp(Lazy.force coq_cutProof,
 	      [| dump_psatz coq_Z dump_z cone ;
 		 dump_proof_term prf|])
  | Micromega.EnumProof(c1,c2,prfs) ->
-    Term.mkApp (Lazy.force coq_enumProof,
-	       [|  dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ;
-		  dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |])
+    EConstr.mkApp (Lazy.force coq_enumProof,
+	           [|  dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ;
+		       dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |])
 
 
 let rec size_of_psatz = function
@@ -1638,11 +1634,11 @@ let parse_goal gl parse_arith env hyps term =
   * The datastructures that aggregate theory-dependent proof values.
   *)
 type ('synt_c, 'prf) domain_spec = {
-  typ : Term.constr; (* is the type of the interpretation domain - Z, Q, R*)
-  coeff : Term.constr ; (* is the type of the syntactic coeffs - Z , Q , Rcst *)
-  dump_coeff : 'synt_c -> Term.constr ; 
-  proof_typ  : Term.constr ; 
-  dump_proof   : 'prf -> Term.constr
+  typ : EConstr.constr; (* is the type of the interpretation domain - Z, Q, R*)
+  coeff : EConstr.constr ; (* is the type of the syntactic coeffs - Z , Q , Rcst *)
+  dump_coeff : 'synt_c -> EConstr.constr ; 
+  proof_typ  : EConstr.constr ; 
+  dump_proof   : 'prf -> EConstr.constr
 }
 
 let zz_domain_spec  = lazy {
@@ -1707,7 +1703,7 @@ let topo_sort_constr 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 ("__v"^(string_of_int i)))) 0 env in *)
- let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in
+ let formula_typ = (EConstr.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) (vm_of_list env) in
  (* todo : directly generate the proof term - or generalize before conversion? *)
@@ -1717,8 +1713,8 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
      Tactics.change_concl
     (set
       [
-       ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
-       ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|]));
+       ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
+       ("__varmap", vm, EConstr.mkApp(Lazy.force coq_VarMap, [|spec.typ|]));
        ("__wit", cert, cert_typ)
       ]
       (Tacmach.New.pf_concl gl))
@@ -1842,20 +1838,20 @@ let abstract_formula hyps f =
       | A(a,t,term) -> if TagSet.mem t hyps then A(a,t,term) else X(term)
       | C(f1,f2) ->
 	  (match xabs f1 , xabs f2 with
-	    |   X a1    ,  X a2   -> X (Term.mkApp(Lazy.force coq_and, [|a1;a2|]))
+	    |   X a1    ,  X a2   -> X (EConstr.mkApp(Lazy.force coq_and, [|a1;a2|]))
 	    |    f1     , f2      -> C(f1,f2) )
       | D(f1,f2) ->
 	  (match xabs f1 , xabs f2 with
-	    |   X a1    ,  X a2   -> X (Term.mkApp(Lazy.force coq_or, [|a1;a2|]))
+	    |   X a1    ,  X a2   -> X (EConstr.mkApp(Lazy.force coq_or, [|a1;a2|]))
 	    |    f1     , f2      -> D(f1,f2) )
       | N(f) ->
 	  (match xabs f with
-	    |   X a    -> X (Term.mkApp(Lazy.force coq_not, [|a|]))
+	    |   X a    -> X (EConstr.mkApp(Lazy.force coq_not, [|a|]))
 	    |     f     -> N f)
       | I(f1,hyp,f2) ->
 	  (match xabs f1 , hyp, xabs f2 with
 	    | X a1      , Some _ , af2    ->  af2
-	    | X a1      , None   , X a2   -> X (Term.mkArrow a1 a2)
+	    | X a1      , None   , X a2   -> X (EConstr.mkArrow a1 a2)
 	    |   af1     ,  _     , af2    -> I(af1,hyp,af2)
 	  )
       | FF -> FF
@@ -1909,7 +1905,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
  if debug then
    begin
      Feedback.msg_notice (Pp.str "Formula....\n") ;
-     let formula_typ = (Term.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
+     let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
      let ff = dump_formula formula_typ
        (dump_cstr spec.typ spec.dump_coeff) ff in
        Feedback.msg_notice (Printer.pr_leconstr ff);
@@ -1934,7 +1930,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
   if debug then
     begin
       Feedback.msg_notice (Pp.str "\nAFormula\n") ;
-      let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
+      let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
       let ff' = dump_formula formula_typ
         (dump_cstr spec.typ spec.dump_coeff) ff' in
         Feedback.msg_notice (Printer.pr_leconstr ff');
@@ -1992,11 +1988,11 @@ let micromega_gen
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
        let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
        let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in
-       let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in 
+       let env' = List.map (fun (id,i) -> EConstr.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
+                                                      (EConstr.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in
 
        let goal_props = List.rev (prop_env_of_formula sigma ff') in 
 
@@ -2015,8 +2011,8 @@ let micromega_gen
          [
            kill_arith;
            (Tacticals.New.tclTHENLIST
-            [(Tactics.generalize (List.map Term.mkVar ids));
-             Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args))
+            [(Tactics.generalize (List.map EConstr.mkVar ids));
+             Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args))
             ] )
          ]
     with
@@ -2044,9 +2040,9 @@ let micromega_order_changer cert env ff  =
   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 cert_typ = (EConstr.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in
  
-  let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
+  let formula_typ = (EConstr.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 begin fun gl -> 
@@ -2055,8 +2051,8 @@ let micromega_order_changer cert env ff  =
      (Tactics.change_concl
       (set
         [
-         ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
-         ("__varmap", vm, Term.mkApp
+         ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
+         ("__varmap", vm, EConstr.mkApp
           (gen_constant_in_modules "VarMap"
 	    [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|]));
          ("__wit", cert, cert_typ)
@@ -2107,7 +2103,7 @@ let micromega_genr prover tac =
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
        let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
        let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in
-       let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in 
+       let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in 
        
        let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
                                                     micromega_order_changer res' env' ff_arith ] in
@@ -2129,8 +2125,8 @@ let micromega_genr prover tac =
          [
            kill_arith;
            (Tacticals.New.tclTHENLIST
-            [(Tactics.generalize (List.map Term.mkVar ids));
-             Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args))
+            [(Tactics.generalize (List.map EConstr.mkVar ids));
+             Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args))
             ] )
          ]
 
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
new file mode 100644
index 0000000000..7da4a3b829
--- /dev/null
+++ b/plugins/micromega/micromega.ml
@@ -0,0 +1,1773 @@
+
+(** val negb : bool -> bool **)
+
+let negb = function
+| true -> false
+| false -> true
+
+type nat =
+| O
+| S of nat
+
+(** val app : 'a1 list -> 'a1 list -> 'a1 list **)
+
+let rec app l m =
+  match l with
+  | [] -> m
+  | a::l1 -> a::(app l1 m)
+
+type comparison =
+| Eq
+| Lt
+| Gt
+
+(** val compOpp : comparison -> comparison **)
+
+let compOpp = function
+| Eq -> Eq
+| Lt -> Gt
+| Gt -> Lt
+
+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
+include Coq__1
+
+type positive =
+| XI of positive
+| XO of positive
+| XH
+
+type n =
+| N0
+| Npos of positive
+
+type z =
+| Z0
+| Zpos of positive
+| Zneg of positive
+
+module Pos =
+ struct
+  type mask =
+  | IsNul
+  | IsPos of positive
+  | IsNeg
+ end
+
+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 ->
+      (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
+
+  type mask = Pos.mask =
+  | IsNul
+  | IsPos of positive
+  | IsNeg
+
+  (** 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 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 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 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 r p q0
+       | XO q0 -> compare_cont Gt p q0
+       | XH -> Gt)
+    | XO p ->
+      (match y with
+       | 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 =
+    compare_cont Eq
+
+  (** 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 _ -> 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 (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)
+ end
+
+module N =
+ struct
+  (** val of_nat : nat -> n **)
+
+  let of_nat = function
+  | O -> N0
+  | S n' -> Npos (Coq_Pos.of_succ_nat n')
+ end
+
+(** val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 **)
+
+let rec pow_pos rmul x = function
+| XI i0 -> let p = pow_pos rmul x i0 in rmul x (rmul p p)
+| XO i0 -> let p = pow_pos rmul x i0 in rmul p p
+| XH -> x
+
+(** val nth : nat -> 'a1 list -> 'a1 -> 'a1 **)
+
+let rec nth n0 l default =
+  match n0 with
+  | O -> (match l with
+          | [] -> default
+          | x::_ -> x)
+  | S m -> (match l with
+            | [] -> default
+            | _::t0 -> nth m t0 default)
+
+(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
+
+let rec map f = function
+| [] -> []
+| 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::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 ->
+      (match y with
+       | XI q0 -> double (pos_sub p q0)
+       | XO q0 -> succ_double (pos_sub p q0)
+       | XH -> Zpos (XO p))
+    | XO p ->
+      (match y with
+       | XI q0 -> pred_double (pos_sub p q0)
+       | XO q0 -> double (pos_sub p q0)
+       | XH -> Zpos (Coq_Pos.pred_double p))
+    | XH ->
+      (match y with
+       | 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
+    | Zpos x' ->
+      (match y with
+       | Z0 -> x
+       | Zpos y' -> Zpos (Coq_Pos.add x' y')
+       | Zneg y' -> pos_sub x' y')
+    | Zneg x' ->
+      (match y with
+       | 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 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
+    | Zpos x' ->
+      (match y with
+       | Z0 -> Z0
+       | Zpos y' -> Zpos (Coq_Pos.mul x' y')
+       | Zneg y' -> Zneg (Coq_Pos.mul x' y'))
+    | Zneg x' ->
+      (match y with
+       | Z0 -> Z0
+       | Zpos y' -> Zneg (Coq_Pos.mul x' y')
+       | Zneg y' -> Zpos (Coq_Pos.mul x' y'))
+
+  (** val compare : z -> z -> comparison **)
+
+  let compare x y =
+    match x with
+    | Z0 -> (match y with
+             | Z0 -> Eq
+             | Zpos _ -> Lt
+             | Zneg _ -> Gt)
+    | Zpos x' -> (match y with
+                  | Zpos y' -> Coq_Pos.compare x' y'
+                  | _ -> Gt)
+    | Zneg x' ->
+      (match y with
+       | Zneg y' -> compOpp (Coq_Pos.compare x' y')
+       | _ -> Lt)
+
+  (** val leb : z -> z -> bool **)
+
+  let leb x y =
+    match compare x y with
+    | Gt -> 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 max : z -> z -> z **)
+
+  let max n0 m =
+    match compare n0 m with
+    | Lt -> m
+    | _ -> n0
+
+  (** val abs : z -> z **)
+
+  let abs = function
+  | Zneg p -> Zpos p
+  | x -> x
+
+  (** val to_N : z -> n **)
+
+  let to_N = function
+  | Zpos p -> Npos p
+  | _ -> N0
+
+  (** 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 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 ltb r' b
+      then (mul (Zpos (XO XH)) q0),r'
+      else (add (mul (Zpos (XO XH)) q0) (Zpos XH)),(sub r' b)
+    | 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 _ -> pos_div_eucl a' b
+       | Zneg b' ->
+         let q0,r = pos_div_eucl a' (Zpos b') in
+         (match r with
+          | Z0 -> (opp q0),Z0
+          | _ -> (opp (add q0 (Zpos XH))),(add b r)))
+    | Zneg a' ->
+      (match b with
+       | Z0 -> Z0,Z0
+       | 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,_ = div_eucl a b in q0
+
+  (** val gcd : z -> z -> z **)
+
+  let gcd a b =
+    match a with
+    | Z0 -> abs b
+    | Zpos a0 ->
+      (match b with
+       | Z0 -> abs a
+       | Zpos b0 -> Zpos (Coq_Pos.gcd a0 b0)
+       | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0))
+    | Zneg a0 ->
+      (match b with
+       | Z0 -> abs a
+       | Zpos b0 -> Zpos (Coq_Pos.gcd a0 b0)
+       | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0))
+ end
+
+(** val zeq_bool : z -> z -> bool **)
+
+let zeq_bool x y =
+  match Z.compare x y with
+  | Eq -> true
+  | _ -> false
+
+type 'c pol =
+| Pc of 'c
+| Pinj of positive * 'c pol
+| PX of 'c pol * positive * 'c pol
+
+(** val p0 : 'a1 -> 'a1 pol **)
+
+let p0 cO =
+  Pc cO
+
+(** val p1 : 'a1 -> 'a1 pol **)
+
+let p1 cI =
+  Pc cI
+
+(** val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool **)
+
+let rec peq ceqb p p' =
+  match p with
+  | Pc c -> (match p' with
+             | Pc c' -> ceqb c c'
+             | _ -> false)
+  | Pinj (j, q0) ->
+    (match p' with
+     | Pinj (j', q') ->
+       (match Coq_Pos.compare j j' with
+        | Eq -> peq ceqb q0 q'
+        | _ -> false)
+     | _ -> false)
+  | PX (p2, i, q0) ->
+    (match p' with
+     | PX (p'0, i', q') ->
+       (match Coq_Pos.compare i i' with
+        | Eq -> if peq ceqb p2 p'0 then peq ceqb q0 q' else false
+        | _ -> false)
+     | _ -> false)
+
+(** val mkPinj : positive -> 'a1 pol -> 'a1 pol **)
+
+let mkPinj j p = match p with
+| Pc _ -> p
+| Pinj (j', q0) -> Pinj ((Coq_Pos.add j j'), q0)
+| PX (_, _, _) -> Pinj (j, p)
+
+(** val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol **)
+
+let mkPinj_pred j p =
+  match j with
+  | XI j0 -> Pinj ((XO j0), p)
+  | XO j0 -> Pinj ((Coq_Pos.pred_double j0), p)
+  | XH -> p
+
+(** val mkPX :
+    '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 (_, _) -> PX (p, i, q0)
+  | PX (p', i', q') ->
+    if peq ceqb q' (p0 cO)
+    then PX (p', (Coq_Pos.add i' i), q0)
+    else PX (p, i, q0)
+
+(** val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol **)
+
+let mkXi cO cI i =
+  PX ((p1 cI), i, (p0 cO))
+
+(** val mkX : 'a1 -> 'a1 -> 'a1 pol **)
+
+let mkX cO cI =
+  mkXi cO cI XH
+
+(** val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol **)
+
+let rec popp copp = function
+| Pc c -> Pc (copp c)
+| Pinj (j, q0) -> Pinj (j, (popp copp q0))
+| PX (p2, i, q0) -> PX ((popp copp p2), i, (popp copp q0))
+
+(** val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol **)
+
+let rec paddC cadd p c =
+  match p with
+  | Pc c1 -> Pc (cadd c1 c)
+  | Pinj (j, q0) -> Pinj (j, (paddC cadd q0 c))
+  | PX (p2, i, q0) -> PX (p2, i, (paddC cadd q0 c))
+
+(** val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol **)
+
+let rec psubC csub p c =
+  match p with
+  | Pc c1 -> Pc (csub c1 c)
+  | Pinj (j, q0) -> Pinj (j, (psubC csub q0 c))
+  | PX (p2, i, q0) -> PX (p2, i, (psubC csub q0 c))
+
+(** val paddI :
+    ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol ->
+    positive -> 'a1 pol -> 'a1 pol **)
+
+let rec paddI cadd pop q0 j = function
+| Pc c -> mkPinj j (paddC cadd q0 c)
+| Pinj (j', q') ->
+  (match Z.pos_sub j' j with
+   | Z0 -> mkPinj j (pop q' q0)
+   | Zpos k -> mkPinj j (pop (Pinj (k, q')) q0)
+   | Zneg k -> mkPinj j' (paddI cadd pop q0 k q'))
+| PX (p2, i, q') ->
+  (match j with
+   | XI j0 -> PX (p2, i, (paddI cadd pop q0 (XO j0) q'))
+   | XO j0 -> PX (p2, i, (paddI cadd pop q0 (Coq_Pos.pred_double j0) q'))
+   | 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 **)
+
+let rec psubI cadd copp pop q0 j = function
+| Pc c -> mkPinj j (paddC cadd (popp copp q0) c)
+| Pinj (j', q') ->
+  (match Z.pos_sub j' j with
+   | Z0 -> mkPinj j (pop q' q0)
+   | Zpos k -> mkPinj j (pop (Pinj (k, q')) q0)
+   | Zneg k -> mkPinj j' (psubI cadd copp pop q0 k q'))
+| PX (p2, i, q') ->
+  (match j with
+   | XI j0 -> PX (p2, i, (psubI cadd copp pop q0 (XO j0) q'))
+   | XO j0 -> PX (p2, i, (psubI cadd copp pop q0 (Coq_Pos.pred_double j0) q'))
+   | 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 **)
+
+let rec paddX cO ceqb pop p' i' p = match p with
+| Pc _ -> PX (p', i', p)
+| Pinj (j, q') ->
+  (match j with
+   | XI j0 -> PX (p', i', (Pinj ((XO j0), q')))
+   | XO j0 -> PX (p', i', (Pinj ((Coq_Pos.pred_double j0), q')))
+   | XH -> PX (p', i', q'))
+| PX (p2, i, q') ->
+  (match Z.pos_sub i i' with
+   | Z0 -> mkPX cO ceqb (pop p2 p') i q'
+   | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q'
+   | 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 **)
+
+let rec psubX cO copp ceqb pop p' i' p = match p with
+| 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')))
+   | XH -> PX ((popp copp p'), i', q'))
+| PX (p2, i, q') ->
+  (match Z.pos_sub i i' with
+   | Z0 -> mkPX cO ceqb (pop p2 p') i q'
+   | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q'
+   | 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 **)
+
+let rec padd cO cadd ceqb p = function
+| Pc c' -> paddC cadd p c'
+| Pinj (j', q') -> paddI cadd (padd cO cadd ceqb) q' j' p
+| PX (p'0, i', q') ->
+  (match p with
+   | Pc c -> PX (p'0, i', (paddC cadd q' c))
+   | Pinj (j, q0) ->
+     (match j with
+      | XI j0 -> PX (p'0, i', (padd cO cadd ceqb (Pinj ((XO j0), q0)) q'))
+      | XO j0 ->
+        PX (p'0, i',
+          (padd cO cadd ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) q'))
+      | XH -> PX (p'0, i', (padd cO cadd ceqb q0 q')))
+   | 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')
+      | Zpos k ->
+        mkPX cO ceqb (padd cO cadd ceqb (PX (p2, k, (p0 cO))) p'0) i'
+          (padd cO cadd ceqb q0 q')
+      | Zneg k ->
+        mkPX cO ceqb (paddX cO ceqb (padd cO cadd ceqb) p'0 k p2) i
+          (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 **)
+
+let rec psub cO cadd csub copp ceqb p = function
+| Pc c' -> psubC csub p c'
+| Pinj (j', q') -> psubI cadd copp (psub cO cadd csub copp ceqb) q' j' p
+| PX (p'0, i', q') ->
+  (match p with
+   | Pc c -> PX ((popp copp p'0), i', (paddC cadd (popp copp q') c))
+   | Pinj (j, q0) ->
+     (match j with
+      | XI j0 ->
+        PX ((popp copp p'0), i',
+          (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')))
+   | 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')
+      | 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 **)
+
+let rec pmulC_aux cO cmul ceqb p c =
+  match p with
+  | Pc c' -> Pc (cmul c' c)
+  | Pinj (j, q0) -> mkPinj j (pmulC_aux cO cmul ceqb q0 c)
+  | PX (p2, i, q0) ->
+    mkPX cO ceqb (pmulC_aux cO cmul ceqb p2 c) i (pmulC_aux cO cmul ceqb q0 c)
+
+(** val pmulC :
+    '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
+  then p0 cO
+  else if ceqb c cI then p else pmulC_aux cO cmul ceqb p c
+
+(** val pmulI :
+    'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol ->
+    '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)
+| Pinj (j', q') ->
+  (match Z.pos_sub j' j with
+   | Z0 -> mkPinj j (pmul0 q' q0)
+   | Zpos k -> mkPinj j (pmul0 (Pinj (k, q')) q0)
+   | Zneg k -> mkPinj j' (pmulI cO cI cmul ceqb pmul0 q0 k q'))
+| PX (p', i', q') ->
+  (match j with
+   | XI j' ->
+     mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i'
+       (pmulI cO cI cmul ceqb pmul0 q0 (XO j') q')
+   | XO j' ->
+     mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i'
+       (pmulI cO cI cmul ceqb pmul0 q0 (Coq_Pos.pred_double j') q')
+   | XH ->
+     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 **)
+
+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
+| PX (p', i', q') ->
+  (match p with
+   | Pc c -> pmulC cO cI cmul ceqb p'' c
+   | Pinj (j, q0) ->
+     let qQ' =
+       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'
+       | 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 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'))
+
+(** val psquare :
+    '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)
+| Pinj (j, q0) -> Pinj (j, (psquare cO cI cadd cmul ceqb q0))
+| PX (p2, i, q0) ->
+  let twoPQ =
+    pmul cO cI cadd cmul ceqb p2
+      (mkPinj XH (pmulC cO cI cmul ceqb q0 (cadd cI cI)))
+  in
+  let q2 = psquare cO cI cadd cmul ceqb q0 in
+  let p3 = psquare cO cI cadd cmul ceqb p2 in
+  mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb p3 i (p0 cO)) twoPQ) i q2
+
+type 'c pExpr =
+| PEc of 'c
+| PEX of positive
+| PEadd of 'c pExpr * 'c pExpr
+| PEsub of 'c pExpr * 'c pExpr
+| PEmul of 'c pExpr * 'c pExpr
+| PEopp of 'c pExpr
+| PEpow of 'c pExpr * n
+
+(** val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol **)
+
+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 **)
+
+let rec ppow_pos cO cI cadd cmul ceqb subst_l res p = function
+| XI p3 ->
+  subst_l
+    (pmul cO cI cadd cmul ceqb
+      (ppow_pos cO cI cadd cmul ceqb subst_l
+        (ppow_pos cO cI cadd cmul ceqb subst_l res p p3) p p3) p)
+| XO p3 ->
+  ppow_pos cO cI cadd cmul ceqb subst_l
+    (ppow_pos cO cI cadd cmul ceqb subst_l res p p3) p p3
+| 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 **)
+
+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 **)
+
+let rec norm_aux cO cI cadd cmul csub copp ceqb = function
+| PEc c -> Pc c
+| PEX j -> mk_X cO cI j
+| PEadd (pe1, pe2) ->
+  (match pe1 with
+   | PEopp pe3 ->
+     psub cO cadd csub copp ceqb
+       (norm_aux cO cI cadd cmul csub copp ceqb pe2)
+       (norm_aux cO cI cadd cmul csub copp ceqb pe3)
+   | _ ->
+     (match pe2 with
+      | PEopp pe3 ->
+        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 pe3)
+      | _ ->
+        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)
+    (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)
+    (norm_aux cO cI cadd cmul csub copp ceqb pe2)
+| PEopp pe1 -> popp copp (norm_aux cO cI cadd cmul csub copp ceqb pe1)
+| PEpow (pe1, n0) ->
+  ppow_N cO cI cadd cmul ceqb (fun p -> p)
+    (norm_aux cO cI cadd cmul csub copp ceqb pe1) n0
+
+type 'a bFormula =
+| TT
+| FF
+| X
+| A of 'a
+| Cj of 'a bFormula * 'a bFormula
+| D of 'a bFormula * 'a bFormula
+| N of 'a bFormula
+| I of 'a bFormula * 'a bFormula
+
+(** val map_bformula : ('a1 -> 'a2) -> 'a1 bFormula -> 'a2 bFormula **)
+
+let rec map_bformula fct = function
+| TT -> TT
+| FF -> FF
+| X -> X
+| A a -> A (fct a)
+| Cj (f1, f2) -> Cj ((map_bformula fct f1), (map_bformula fct f2))
+| D (f1, f2) -> D ((map_bformula fct f1), (map_bformula fct f2))
+| N f0 -> N (map_bformula fct f0)
+| I (f1, f2) -> I ((map_bformula fct f1), (map_bformula fct f2))
+
+type 'x clause = 'x list
+
+type 'x cnf = 'x clause list
+
+(** val tt : 'a1 cnf **)
+
+let tt =
+  []
+
+(** val ff : 'a1 cnf **)
+
+let ff =
+  []::[]
+
+(** val add_term :
+    ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> 'a1
+    clause option **)
+
+let rec add_term unsat deduce t0 = function
+| [] ->
+  (match deduce t0 t0 with
+   | Some u -> if unsat u then None else Some (t0::[])
+   | None -> Some (t0::[]))
+| t'::cl0 ->
+  (match deduce t0 t' with
+   | Some u ->
+     if unsat u
+     then None
+     else (match add_term unsat deduce t0 cl0 with
+           | Some cl' -> Some (t'::cl')
+           | None -> None)
+   | None ->
+     (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 **)
+
+let rec or_clause unsat deduce cl1 cl2 =
+  match cl1 with
+  | [] -> Some cl2
+  | 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 **)
+
+let or_clause_cnf unsat deduce t0 f =
+  fold_right (fun e acc ->
+    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 **)
+
+let rec or_cnf unsat deduce f f' =
+  match f with
+  | [] -> tt
+  | e::rst ->
+    app (or_cnf unsat deduce rst f') (or_clause_cnf unsat deduce e f')
+
+(** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **)
+
+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 **)
+
+let rec xcnf unsat deduce normalise0 negate0 pol0 = function
+| TT -> if pol0 then tt else ff
+| FF -> if pol0 then ff else tt
+| X -> ff
+| A x -> if pol0 then normalise0 x else negate0 x
+| Cj (e1, e2) ->
+  if pol0
+  then and_cnf (xcnf unsat deduce normalise0 negate0 pol0 e1)
+         (xcnf unsat deduce normalise0 negate0 pol0 e2)
+  else or_cnf unsat deduce (xcnf unsat deduce normalise0 negate0 pol0 e1)
+         (xcnf unsat deduce normalise0 negate0 pol0 e2)
+| D (e1, e2) ->
+  if pol0
+  then or_cnf unsat deduce (xcnf unsat deduce normalise0 negate0 pol0 e1)
+         (xcnf unsat deduce normalise0 negate0 pol0 e2)
+  else and_cnf (xcnf unsat deduce normalise0 negate0 pol0 e1)
+         (xcnf unsat deduce normalise0 negate0 pol0 e2)
+| N e -> xcnf unsat deduce normalise0 negate0 (negb pol0) e
+| I (e1, e2) ->
+  if pol0
+  then or_cnf unsat deduce
+         (xcnf unsat deduce normalise0 negate0 (negb pol0) e1)
+         (xcnf unsat deduce normalise0 negate0 pol0 e2)
+  else and_cnf (xcnf unsat deduce normalise0 negate0 (negb pol0) e1)
+         (xcnf unsat deduce normalise0 negate0 pol0 e2)
+
+(** val cnf_checker :
+    ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool **)
+
+let rec cnf_checker checker f l =
+  match f with
+  | [] -> true
+  | e::f0 ->
+    (match l with
+     | [] -> false
+     | 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 **)
+
+let tauto_checker unsat deduce normalise0 negate0 checker f w =
+  cnf_checker checker (xcnf unsat deduce normalise0 negate0 true f) w
+
+(** val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool **)
+
+let cneqb ceqb x y =
+  negb (ceqb x y)
+
+(** val cltb :
+    ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool **)
+
+let cltb ceqb cleb x y =
+  (&&) (cleb x y) (cneqb ceqb x y)
+
+type 'c polC = 'c pol
+
+type op1 =
+| Equal
+| NonEqual
+| Strict
+| NonStrict
+
+type 'c nFormula = 'c polC * op1
+
+(** val opMult : op1 -> op1 -> op1 option **)
+
+let opMult o o' =
+  match o with
+  | Equal -> Some Equal
+  | NonEqual ->
+    (match o' with
+     | Equal -> Some Equal
+     | NonEqual -> Some NonEqual
+     | _ -> None)
+  | Strict -> (match o' with
+               | NonEqual -> None
+               | _ -> Some o')
+  | NonStrict ->
+    (match o' with
+     | Equal -> Some Equal
+     | NonEqual -> None
+     | _ -> Some NonStrict)
+
+(** val opAdd : op1 -> op1 -> op1 option **)
+
+let opAdd o o' =
+  match o with
+  | Equal -> Some o'
+  | NonEqual -> (match o' with
+                 | Equal -> Some NonEqual
+                 | _ -> None)
+  | Strict -> (match o' with
+               | NonEqual -> None
+               | _ -> Some Strict)
+  | NonStrict ->
+    (match o' with
+     | Equal -> Some NonStrict
+     | NonEqual -> None
+     | x -> Some x)
+
+type 'c psatz =
+| PsatzIn of nat
+| PsatzSquare of 'c polC
+| PsatzMulC of 'c polC * 'c psatz
+| PsatzMulE of 'c psatz * 'c psatz
+| PsatzAdd of 'c psatz * 'c psatz
+| PsatzC of 'c
+| PsatzZ
+
+(** val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option **)
+
+let map_option f = function
+| Some x -> f x
+| None -> None
+
+(** val map_option2 :
+    ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option **)
+
+let map_option2 f o o' =
+  match o with
+  | Some x -> (match o' with
+               | Some x' -> f x x'
+               | None -> None)
+  | None -> None
+
+(** val pexpr_times_nformula :
+    '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 ->
+  (match o with
+   | Equal -> Some ((pmul cO cI cplus ctimes ceqb e ef),Equal)
+   | _ -> None)
+
+(** val nformula_times_nformula :
+    '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
+  let e2,o2 = f2 in
+  map_option (fun x -> Some ((pmul cO cI cplus ctimes ceqb e1 e2),x))
+    (opMult o1 o2)
+
+(** val nformula_plus_nformula :
+    '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
+  let e2,o2 = f2 in
+  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 **)
+
+let rec eval_Psatz cO cI cplus ctimes ceqb cleb l = function
+| PsatzIn n0 -> Some (nth n0 l ((Pc cO),Equal))
+| PsatzSquare e0 -> Some ((psquare cO cI cplus ctimes ceqb e0),NonStrict)
+| PsatzMulC (re, e0) ->
+  map_option (pexpr_times_nformula cO cI cplus ctimes ceqb re)
+    (eval_Psatz cO cI cplus ctimes ceqb cleb l e0)
+| PsatzMulE (f1, f2) ->
+  map_option2 (nformula_times_nformula cO cI cplus ctimes ceqb)
+    (eval_Psatz cO cI cplus ctimes ceqb cleb l f1)
+    (eval_Psatz cO cI cplus ctimes ceqb cleb l f2)
+| PsatzAdd (f1, f2) ->
+  map_option2 (nformula_plus_nformula cO cplus ceqb)
+    (eval_Psatz cO cI cplus ctimes ceqb cleb l f1)
+    (eval_Psatz cO cI cplus ctimes ceqb cleb l f2)
+| PsatzC c -> if cltb ceqb cleb cO c then Some ((Pc c),Strict) else None
+| PsatzZ -> Some ((Pc cO),Equal)
+
+(** val check_inconsistent :
+    'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula ->
+    bool **)
+
+let check_inconsistent cO ceqb cleb = function
+| e,op ->
+  (match e with
+   | Pc c ->
+     (match op with
+      | Equal -> cneqb ceqb c cO
+      | NonEqual -> ceqb c cO
+      | Strict -> cleb c cO
+      | NonStrict -> cltb ceqb cleb c cO)
+   | _ -> 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 **)
+
+let check_normalised_formulas cO cI cplus ctimes ceqb cleb l cm =
+  match eval_Psatz cO cI cplus ctimes ceqb cleb l cm with
+  | Some f -> check_inconsistent cO ceqb cleb f
+  | None -> false
+
+type op2 =
+| OpEq
+| OpNEq
+| OpLe
+| OpGe
+| OpLt
+| OpGt
+
+type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr }
+
+(** val norm :
+    '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 **)
+
+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 **)
+
+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 **)
+
+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
+                                                               cminus copp
+                                                               ceqb rhs0 lhs0),Strict)::[])
+   | OpNEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Equal)::[]
+   | OpLe -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::[]
+   | OpGe -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),Strict)::[]
+   | OpLt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),NonStrict)::[]
+   | 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 **)
+
+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 **)
+
+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
+                                                               cminus copp
+                                                               ceqb rhs0 lhs0),Strict)::[])
+   | OpLe -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),NonStrict)::[]
+   | OpGe -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),NonStrict)::[]
+   | OpLt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),Strict)::[]
+   | 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 **)
+
+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 **)
+
+let rec xdenorm jmp = function
+| Pc c -> PEc c
+| Pinj (j, p2) -> xdenorm (Coq_Pos.add j jmp) p2
+| PX (p2, j, q0) ->
+  PEadd ((PEmul ((xdenorm jmp p2), (PEpow ((PEX jmp), (Npos j))))),
+    (xdenorm (Coq_Pos.succ jmp) q0))
+
+(** val denorm : 'a1 pol -> 'a1 pExpr **)
+
+let denorm p =
+  xdenorm XH p
+
+(** val map_PExpr : ('a2 -> 'a1) -> 'a2 pExpr -> 'a1 pExpr **)
+
+let rec map_PExpr c_of_S = function
+| PEc c -> PEc (c_of_S c)
+| PEX p -> PEX p
+| PEadd (e1, e2) -> PEadd ((map_PExpr c_of_S e1), (map_PExpr c_of_S e2))
+| PEsub (e1, e2) -> PEsub ((map_PExpr c_of_S e1), (map_PExpr c_of_S e2))
+| PEmul (e1, e2) -> PEmul ((map_PExpr c_of_S e1), (map_PExpr c_of_S e2))
+| PEopp e0 -> PEopp (map_PExpr c_of_S e0)
+| PEpow (e0, n0) -> PEpow ((map_PExpr c_of_S e0), n0)
+
+(** val map_Formula : ('a2 -> 'a1) -> 'a2 formula -> 'a1 formula **)
+
+let map_Formula c_of_S f =
+  let { flhs = l; fop = o; frhs = r } = f in
+  { 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 **)
+
+let simpl_cone cO cI ctimes ceqb e = match e with
+| PsatzSquare t0 ->
+  (match t0 with
+   | Pc c -> if ceqb cO c then PsatzZ else PsatzC (ctimes c c)
+   | _ -> PsatzSquare t0)
+| PsatzMulE (t1, t2) ->
+  (match t1 with
+   | PsatzMulE (x, x0) ->
+     (match x with
+      | PsatzC p2 ->
+        (match t2 with
+         | PsatzC c -> PsatzMulE ((PsatzC (ctimes c p2)), x0)
+         | PsatzZ -> PsatzZ
+         | _ -> e)
+      | _ ->
+        (match x0 with
+         | PsatzC p2 ->
+           (match t2 with
+            | PsatzC c -> PsatzMulE ((PsatzC (ctimes c p2)), x)
+            | PsatzZ -> PsatzZ
+            | _ -> e)
+         | _ ->
+           (match t2 with
+            | PsatzC c -> if ceqb cI c then t1 else PsatzMulE (t1, t2)
+            | PsatzZ -> PsatzZ
+            | _ -> e)))
+   | PsatzC c ->
+     (match t2 with
+      | PsatzMulE (x, x0) ->
+        (match x with
+         | PsatzC p2 -> PsatzMulE ((PsatzC (ctimes c p2)), x0)
+         | _ ->
+           (match x0 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)))
+      | PsatzC c0 -> PsatzC (ctimes c c0)
+      | PsatzZ -> PsatzZ
+      | _ -> if ceqb cI c then t2 else PsatzMulE (t1, t2))
+   | PsatzZ -> PsatzZ
+   | _ ->
+     (match t2 with
+      | PsatzC c -> if ceqb cI c then t1 else PsatzMulE (t1, t2)
+      | PsatzZ -> PsatzZ
+      | _ -> e))
+| PsatzAdd (t1, t2) ->
+  (match t1 with
+   | PsatzZ -> t2
+   | _ -> (match t2 with
+           | PsatzZ -> t1
+           | _ -> PsatzAdd (t1, t2)))
+| _ -> e
+
+type q = { qnum : z; qden : positive }
+
+(** val qnum : q -> z **)
+
+let qnum x = x.qnum
+
+(** val qden : q -> positive **)
+
+let qden x = x.qden
+
+(** val qeq_bool : q -> q -> bool **)
+
+let qeq_bool x y =
+  zeq_bool (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))
+
+(** val qle_bool : q -> q -> bool **)
+
+let qle_bool x y =
+  Z.leb (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))
+
+(** 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)));
+    qden = (Coq_Pos.mul x.qden y.qden) }
+
+(** val qmult : q -> q -> q **)
+
+let qmult x y =
+  { qnum = (Z.mul x.qnum y.qnum); qden = (Coq_Pos.mul x.qden y.qden) }
+
+(** val qopp : q -> q **)
+
+let qopp x =
+  { qnum = (Z.opp x.qnum); qden = x.qden }
+
+(** val qminus : q -> q -> q **)
+
+let qminus x y =
+  qplus x (qopp y)
+
+(** val qinv : q -> q **)
+
+let qinv x =
+  match x.qnum with
+  | Z0 -> { qnum = Z0; qden = XH }
+  | Zpos p -> { qnum = (Zpos x.qden); qden = p }
+  | Zneg p -> { qnum = (Zneg x.qden); qden = p }
+
+(** val qpower_positive : q -> positive -> q **)
+
+let qpower_positive =
+  pow_pos qmult
+
+(** val qpower : q -> z -> q **)
+
+let qpower q0 = function
+| Z0 -> { qnum = (Zpos XH); qden = XH }
+| Zpos p -> qpower_positive q0 p
+| Zneg p -> qinv (qpower_positive q0 p)
+
+type 'a t =
+| Empty
+| Leaf of 'a
+| Node of 'a t * 'a * 'a t
+
+(** val find : 'a1 -> 'a1 t -> positive -> 'a1 **)
+
+let rec find default vm p =
+  match vm with
+  | Empty -> default
+  | Leaf i -> i
+  | Node (l, e, r) ->
+    (match p with
+     | XI p2 -> find default r p2
+     | 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 **)
+
+let zWeakChecker =
+  check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb
+
+(** val psub1 : z pol -> z pol -> z pol **)
+
+let psub1 =
+  psub0 Z0 Z.add Z.sub Z.opp zeq_bool
+
+(** val padd1 : z pol -> z pol -> z pol **)
+
+let padd1 =
+  padd0 Z0 Z.add zeq_bool
+
+(** val norm0 : z pExpr -> z pol **)
+
+let norm0 =
+  norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp zeq_bool
+
+(** val xnormalise0 : z formula -> z nFormula list **)
+
+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
+   | OpEq ->
+     ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::(((psub1 rhs0
+                                                               (padd1 lhs0
+                                                                 (Pc (Zpos
+                                                                 XH)))),NonStrict)::[])
+   | OpNEq -> ((psub1 lhs0 rhs0),Equal)::[]
+   | OpLe -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::[]
+   | OpGe -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))),NonStrict)::[]
+   | OpLt -> ((psub1 lhs0 rhs0),NonStrict)::[]
+   | OpGt -> ((psub1 rhs0 lhs0),NonStrict)::[])
+
+(** val normalise : z formula -> z nFormula cnf **)
+
+let normalise t0 =
+  map (fun x -> x::[]) (xnormalise0 t0)
+
+(** val xnegate0 : z formula -> z nFormula list **)
+
+let xnegate0 t0 =
+  let { flhs = lhs; fop = o; frhs = rhs } = t0 in
+  let lhs0 = norm0 lhs in
+  let rhs0 = norm0 rhs in
+  (match o with
+   | OpEq -> ((psub1 lhs0 rhs0),Equal)::[]
+   | OpNEq ->
+     ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::(((psub1 rhs0
+                                                               (padd1 lhs0
+                                                                 (Pc (Zpos
+                                                                 XH)))),NonStrict)::[])
+   | OpLe -> ((psub1 rhs0 lhs0),NonStrict)::[]
+   | OpGe -> ((psub1 lhs0 rhs0),NonStrict)::[]
+   | OpLt -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))),NonStrict)::[]
+   | OpGt -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::[])
+
+(** val negate : z formula -> z nFormula cnf **)
+
+let negate t0 =
+  map (fun x -> x::[]) (xnegate0 t0)
+
+(** val zunsat : z nFormula -> bool **)
+
+let zunsat =
+  check_inconsistent Z0 zeq_bool Z.leb
+
+(** val zdeduce : z nFormula -> z nFormula -> z nFormula option **)
+
+let zdeduce =
+  nformula_plus_nformula Z0 Z.add zeq_bool
+
+(** val ceiling : z -> z -> z **)
+
+let ceiling a b =
+  let q0,r = Z.div_eucl a b in
+  (match r with
+   | Z0 -> q0
+   | _ -> Z.add q0 (Zpos XH))
+
+type zArithProof =
+| DoneProof
+| RatProof of zWitness * zArithProof
+| CutProof of zWitness * zArithProof
+| EnumProof of zWitness * zWitness * zArithProof list
+
+(** val zgcdM : z -> z -> z **)
+
+let zgcdM x y =
+  Z.max (Z.gcd x y) (Zpos XH)
+
+(** val zgcd_pol : z polC -> z * z **)
+
+let rec zgcd_pol = function
+| Pc c -> Z0,c
+| 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
+
+(** val zdiv_pol : z polC -> z -> z polC **)
+
+let rec zdiv_pol p x =
+  match p with
+  | Pc c -> Pc (Z.div c x)
+  | Pinj (j, p2) -> Pinj (j, (zdiv_pol p2 x))
+  | PX (p2, j, q0) -> PX ((zdiv_pol p2 x), j, (zdiv_pol q0 x))
+
+(** val makeCuttingPlane : z polC -> z polC * z **)
+
+let makeCuttingPlane p =
+  let g,c = zgcd_pol p in
+  if Z.gtb g Z0
+  then (zdiv_pol (psubC Z.sub p c) g),(Z.opp (ceiling (Z.opp c) g))
+  else p,Z0
+
+(** val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option **)
+
+let genCuttingPlane = function
+| e,op ->
+  (match op with
+   | Equal ->
+     let g,c = zgcd_pol e in
+     if (&&) (Z.gtb g Z0)
+          ((&&) (negb (zeq_bool c Z0)) (negb (zeq_bool (Z.gcd g c) g)))
+     then None
+     else Some ((makeCuttingPlane e),Equal)
+   | NonEqual -> Some ((e,Z0),op)
+   | 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 **)
+
+let nformula_of_cutting_plane = function
+| e_z,o -> let e,z0 = e_z in (padd1 e (Pc z0)),o
+
+(** val is_pol_Z0 : z polC -> bool **)
+
+let is_pol_Z0 = function
+| Pc z0 -> (match z0 with
+            | Z0 -> true
+            | _ -> false)
+| _ -> false
+
+(** val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option **)
+
+let eval_Psatz0 =
+  eval_Psatz Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb
+
+(** val valid_cut_sign : op1 -> bool **)
+
+let valid_cut_sign = function
+| Equal -> true
+| NonStrict -> true
+| _ -> false
+
+(** val zChecker : z nFormula list -> zArithProof -> bool **)
+
+let rec zChecker l = function
+| DoneProof -> false
+| RatProof (w, pf0) ->
+  (match eval_Psatz0 l w with
+   | Some f -> if zunsat f then true else zChecker (f::l) pf0
+   | None -> false)
+| CutProof (w, pf0) ->
+  (match eval_Psatz0 l w with
+   | Some f ->
+     (match genCuttingPlane f with
+      | Some cp -> zChecker ((nformula_of_cutting_plane cp)::l) pf0
+      | None -> true)
+   | None -> false)
+| EnumProof (w1, w2, pf0) ->
+  (match eval_Psatz0 l w1 with
+   | Some f1 ->
+     (match eval_Psatz0 l w2 with
+      | Some f2 ->
+        (match genCuttingPlane f1 with
+         | Some p ->
+           let p2,op3 = p in
+           let e1,z1 = p2 in
+           (match genCuttingPlane f2 with
+            | Some p3 ->
+              let p4,op4 = p3 in
+              let e2,z2 = p4 in
+              if (&&) ((&&) (valid_cut_sign op3) (valid_cut_sign op4))
+                   (is_pol_Z0 (padd1 e1 e2))
+              then let rec label pfs lb ub =
+                     match pfs with
+                     | [] -> Z.gtb lb ub
+                     | pf1::rsr ->
+                       (&&) (zChecker (((psub1 e1 (Pc lb)),Equal)::l) pf1)
+                         (label rsr (Z.add lb (Zpos XH)) ub)
+                   in label pf0 (Z.opp z1) z2
+              else false
+            | None -> true)
+         | None -> true)
+      | None -> false)
+   | None -> false)
+
+(** val zTautoChecker : z formula bFormula -> zArithProof list -> bool **)
+
+let zTautoChecker f w =
+  tauto_checker zunsat zdeduce normalise negate zChecker f w
+
+type qWitness = q psatz
+
+(** val qWeakChecker : q nFormula list -> q psatz -> bool **)
+
+let qWeakChecker =
+  check_normalised_formulas { qnum = Z0; qden = XH } { qnum = (Zpos XH);
+    qden = XH } qplus qmult qeq_bool qle_bool
+
+(** val qnormalise : q formula -> q nFormula cnf **)
+
+let qnormalise =
+  cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH }
+    qplus qmult qminus qopp qeq_bool
+
+(** 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
+
+(** val qunsat : q nFormula -> bool **)
+
+let qunsat =
+  check_inconsistent { qnum = Z0; qden = XH } qeq_bool qle_bool
+
+(** val qdeduce : q nFormula -> q nFormula -> q nFormula option **)
+
+let qdeduce =
+  nformula_plus_nformula { qnum = Z0; qden = XH } qplus qeq_bool
+
+(** val qTautoChecker : q formula bFormula -> qWitness list -> bool **)
+
+let qTautoChecker f w =
+  tauto_checker qunsat qdeduce qnormalise qnegate qWeakChecker f w
+
+type rcst =
+| C0
+| C1
+| CQ of q
+| CZ of z
+| CPlus of rcst * rcst
+| CMinus of rcst * rcst
+| CMult of rcst * rcst
+| CInv of rcst
+| COpp of rcst
+
+(** val q_of_Rcst : rcst -> q **)
+
+let rec q_of_Rcst = function
+| C0 -> { qnum = Z0; qden = XH }
+| C1 -> { qnum = (Zpos XH); qden = XH }
+| CQ q0 -> q0
+| CZ z0 -> { qnum = z0; qden = XH }
+| CPlus (r1, r2) -> qplus (q_of_Rcst r1) (q_of_Rcst r2)
+| CMinus (r1, r2) -> qminus (q_of_Rcst r1) (q_of_Rcst r2)
+| CMult (r1, r2) -> qmult (q_of_Rcst r1) (q_of_Rcst r2)
+| CInv r0 -> qinv (q_of_Rcst r0)
+| COpp r0 -> qopp (q_of_Rcst r0)
+
+type rWitness = q psatz
+
+(** val rWeakChecker : q nFormula list -> q psatz -> bool **)
+
+let rWeakChecker =
+  check_normalised_formulas { qnum = Z0; qden = XH } { qnum = (Zpos XH);
+    qden = XH } qplus qmult qeq_bool qle_bool
+
+(** val rnormalise : q formula -> q nFormula cnf **)
+
+let rnormalise =
+  cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH }
+    qplus qmult qminus qopp qeq_bool
+
+(** 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
+
+(** val runsat : q nFormula -> bool **)
+
+let runsat =
+  check_inconsistent { qnum = Z0; qden = XH } qeq_bool qle_bool
+
+(** val rdeduce : q nFormula -> q nFormula -> q nFormula option **)
+
+let rdeduce =
+  nformula_plus_nformula { qnum = Z0; qden = XH } qplus qeq_bool
+
+(** val rTautoChecker : rcst formula bFormula -> rWitness list -> bool **)
+
+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
new file mode 100644
index 0000000000..9619781786
--- /dev/null
+++ b/plugins/micromega/micromega.mli
@@ -0,0 +1,517 @@
+
+val negb : bool -> bool
+
+type nat =
+| O
+| S of nat
+
+val app : 'a1 list -> 'a1 list -> 'a1 list
+
+type comparison =
+| Eq
+| Lt
+| Gt
+
+val compOpp : comparison -> comparison
+
+val add : nat -> nat -> nat
+
+type positive =
+| XI of positive
+| XO of positive
+| XH
+
+type n =
+| N0
+| Npos of positive
+
+type z =
+| Z0
+| Zpos of positive
+| Zneg of positive
+
+module Pos :
+ sig
+  type mask =
+  | IsNul
+  | IsPos of positive
+  | IsNeg
+ end
+
+module Coq_Pos :
+ sig
+  val succ : positive -> positive
+
+  val add : positive -> positive -> positive
+
+  val add_carry : positive -> positive -> positive
+
+  val pred_double : positive -> positive
+
+  type mask = Pos.mask =
+  | IsNul
+  | IsPos of positive
+  | IsNeg
+
+  val succ_double_mask : mask -> mask
+
+  val double_mask : mask -> mask
+
+  val double_pred_mask : positive -> 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 size_nat : positive -> nat
+
+  val compare_cont : comparison -> positive -> positive -> comparison
+
+  val compare : positive -> positive -> comparison
+
+  val gcdn : nat -> positive -> positive -> positive
+
+  val gcd : positive -> positive -> positive
+
+  val of_succ_nat : nat -> positive
+ end
+
+module N :
+ sig
+  val of_nat : nat -> n
+ end
+
+val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1
+
+val nth : nat -> 'a1 list -> 'a1 -> 'a1
+
+val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
+
+val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1
+
+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 sub : z -> z -> z
+
+  val mul : z -> z -> z
+
+  val compare : z -> z -> comparison
+
+  val leb : z -> z -> bool
+
+  val ltb : z -> z -> bool
+
+  val gtb : z -> z -> bool
+
+  val max : z -> z -> z
+
+  val abs : z -> z
+
+  val to_N : z -> n
+
+  val pos_div_eucl : positive -> z -> z * z
+
+  val div_eucl : z -> z -> z * z
+
+  val div : z -> z -> z
+
+  val gcd : z -> z -> z
+ end
+
+val zeq_bool : z -> z -> bool
+
+type 'c pol =
+| Pc of 'c
+| Pinj of positive * 'c pol
+| PX of 'c pol * positive * 'c pol
+
+val p0 : 'a1 -> 'a1 pol
+
+val p1 : 'a1 -> 'a1 pol
+
+val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool
+
+val mkPinj : positive -> 'a1 pol -> 'a1 pol
+
+val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol
+
+val mkPX :
+  'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
+
+val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol
+
+val mkX : 'a1 -> 'a1 -> 'a1 pol
+
+val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
+
+val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
+
+val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
+
+val paddI :
+  ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol ->
+  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
+
+val paddX :
+  '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
+
+val padd :
+  '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
+
+val pmulC_aux :
+  '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
+
+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
+
+val psquare :
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
+  bool) -> 'a1 pol -> 'a1 pol
+
+type 'c pExpr =
+| PEc of 'c
+| PEX of positive
+| PEadd of 'c pExpr * 'c pExpr
+| PEsub of 'c pExpr * 'c pExpr
+| PEmul of 'c pExpr * 'c pExpr
+| PEopp of 'c pExpr
+| PEpow of 'c pExpr * n
+
+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
+
+val ppow_N :
+  '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
+
+type 'a bFormula =
+| TT
+| FF
+| X
+| A of 'a
+| Cj of 'a bFormula * 'a bFormula
+| D of 'a bFormula * 'a bFormula
+| N of 'a bFormula
+| I of 'a bFormula * 'a bFormula
+
+val map_bformula : ('a1 -> 'a2) -> 'a1 bFormula -> 'a2 bFormula
+
+type 'x clause = 'x list
+
+type 'x cnf = 'x clause list
+
+val tt : 'a1 cnf
+
+val ff : 'a1 cnf
+
+val add_term :
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> 'a1
+  clause option
+
+val or_clause :
+  ('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
+
+val or_cnf :
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> 'a1 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
+
+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
+
+val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
+
+val cltb : ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
+
+type 'c polC = 'c pol
+
+type op1 =
+| Equal
+| NonEqual
+| Strict
+| NonStrict
+
+type 'c nFormula = 'c polC * op1
+
+val opMult : op1 -> op1 -> op1 option
+
+val opAdd : op1 -> op1 -> op1 option
+
+type 'c psatz =
+| PsatzIn of nat
+| PsatzSquare of 'c polC
+| PsatzMulC of 'c polC * 'c psatz
+| PsatzMulE of 'c psatz * 'c psatz
+| PsatzAdd of 'c psatz * 'c psatz
+| PsatzC of 'c
+| PsatzZ
+
+val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option
+
+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
+
+val nformula_times_nformula :
+  '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
+
+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
+
+val check_inconsistent :
+  '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
+
+type op2 =
+| OpEq
+| OpNEq
+| OpLe
+| OpGe
+| OpLt
+| OpGt
+
+type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr }
+
+val norm :
+  '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
+
+val padd0 :
+  '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
+
+val cnf_normalise :
+  '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
+
+val cnf_negate :
+  '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
+
+val denorm : 'a1 pol -> 'a1 pExpr
+
+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
+
+type q = { qnum : z; qden : positive }
+
+val qnum : q -> z
+
+val qden : q -> positive
+
+val qeq_bool : q -> q -> bool
+
+val qle_bool : q -> q -> bool
+
+val qplus : q -> q -> q
+
+val qmult : q -> q -> q
+
+val qopp : q -> q
+
+val qminus : q -> q -> q
+
+val qinv : q -> q
+
+val qpower_positive : q -> positive -> q
+
+val qpower : q -> z -> q
+
+type 'a t =
+| Empty
+| Leaf of 'a
+| Node of 'a t * 'a * 'a t
+
+val find : 'a1 -> 'a1 t -> positive -> 'a1
+
+val singleton : 'a1 -> positive -> 'a1 -> 'a1 t
+
+val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t
+
+type zWitness = z psatz
+
+val zWeakChecker : z nFormula list -> z psatz -> bool
+
+val psub1 : z pol -> z pol -> z pol
+
+val padd1 : z pol -> z pol -> z pol
+
+val norm0 : z pExpr -> z pol
+
+val xnormalise0 : z formula -> z nFormula list
+
+val normalise : z formula -> z nFormula cnf
+
+val xnegate0 : z formula -> z nFormula list
+
+val negate : z formula -> z nFormula cnf
+
+val zunsat : z nFormula -> bool
+
+val zdeduce : z nFormula -> z nFormula -> z nFormula option
+
+val ceiling : z -> z -> z
+
+type zArithProof =
+| DoneProof
+| RatProof of zWitness * zArithProof
+| CutProof of zWitness * zArithProof
+| EnumProof of zWitness * zWitness * zArithProof list
+
+val zgcdM : z -> z -> z
+
+val zgcd_pol : z polC -> z * z
+
+val zdiv_pol : z polC -> z -> z polC
+
+val makeCuttingPlane : z polC -> z polC * z
+
+val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option
+
+val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula
+
+val is_pol_Z0 : z polC -> bool
+
+val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option
+
+val valid_cut_sign : op1 -> bool
+
+val zChecker : z nFormula list -> zArithProof -> bool
+
+val zTautoChecker : z formula bFormula -> zArithProof list -> bool
+
+type qWitness = q psatz
+
+val qWeakChecker : q nFormula list -> q psatz -> bool
+
+val qnormalise : q formula -> q nFormula cnf
+
+val qnegate : q formula -> q nFormula cnf
+
+val qunsat : q nFormula -> bool
+
+val qdeduce : q nFormula -> q nFormula -> q nFormula option
+
+val qTautoChecker : q formula bFormula -> qWitness list -> bool
+
+type rcst =
+| C0
+| C1
+| CQ of q
+| CZ of z
+| CPlus of rcst * rcst
+| CMinus of rcst * rcst
+| CMult of rcst * rcst
+| CInv of rcst
+| COpp of rcst
+
+val q_of_Rcst : rcst -> q
+
+type rWitness = q psatz
+
+val rWeakChecker : q nFormula list -> q psatz -> bool
+
+val rnormalise : q formula -> q nFormula cnf
+
+val rnegate : q formula -> q nFormula cnf
+
+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/sos_types.mli b/plugins/micromega/sos_types.mli
new file mode 100644
index 0000000000..57c4e50cad
--- /dev/null
+++ b/plugins/micromega/sos_types.mli
@@ -0,0 +1,40 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* The type of positivstellensatz -- used to communicate with sos *)
+
+type vname = string;;
+
+type term =
+| Zero
+| Const of Num.num
+| Var of vname
+| Inv of term
+| Opp of term
+| Add of (term * term)
+| Sub of (term * term)
+| Mul of (term * term)
+| Div of (term * term)
+| Pow of (term * int);;
+
+val output_term : out_channel -> term -> unit
+
+type positivstellensatz =
+   Axiom_eq of int
+ | Axiom_le of int
+ | Axiom_lt of int
+ | Rational_eq of Num.num
+ | Rational_le of Num.num
+ | Rational_lt of Num.num
+ | Square of term
+ | Monoid of int list
+ | Eqmul of term * positivstellensatz
+ | Sum of positivstellensatz * positivstellensatz
+ | Product of positivstellensatz * positivstellensatz;;
+
+val output_psatz : out_channel -> positivstellensatz -> unit