1 files changed, 931 insertions, 149 deletions

diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 3e3ae2c3..bcd61f39 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -1,115 +1,848 @@
+type __ = Obj.t
+
 val negb : bool -> bool
 
 type nat =
-  | O
-  | S of nat
+| O
+| S of nat
 
-type comparison =
-  | Eq
-  | Lt
-  | Gt
+val fst : ('a1 * 'a2) -> 'a1
 
-val compOpp : comparison -> comparison
-
-val plus : nat -> nat -> nat
+val snd : ('a1 * 'a2) -> 'a2
 
 val app : 'a1 list -> 'a1 list -> 'a1 list
 
-val nth : nat -> 'a1 list -> 'a1 -> 'a1
-
-val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
-
-type positive =
-  | XI of positive
-  | XO of positive
-  | XH
-
-val psucc : positive -> positive
-
-val pplus : positive -> positive -> positive
-
-val pplus_carry : positive -> positive -> positive
-
-val p_of_succ_nat : nat -> positive
-
-val pdouble_minus_one : positive -> positive
-
-type positive_mask =
-  | IsNul
-  | IsPos of positive
-  | IsNeg
+type comparison =
+| Eq
+| Lt
+| Gt
 
-val pdouble_plus_one_mask : positive_mask -> positive_mask
+val compOpp : comparison -> comparison
 
-val pdouble_mask : positive_mask -> positive_mask
+type compareSpecT =
+| CompEqT
+| CompLtT
+| CompGtT
 
-val pdouble_minus_two : positive -> positive_mask
+val compareSpec2Type : comparison -> compareSpecT
 
-val pminus_mask : positive -> positive -> positive_mask
+type 'a compSpecT = compareSpecT
 
-val pminus_mask_carry : positive -> positive -> positive_mask
+val compSpec2Type : 'a1 -> 'a1 -> comparison -> 'a1 compSpecT
 
-val pminus : positive -> positive -> positive
+type 'a sig0 =
+  'a
+  (* singleton inductive, whose constructor was exist *)
 
-val pmult : positive -> positive -> positive
+val plus : nat -> nat -> nat
 
-val pcompare : positive -> positive -> comparison -> comparison
+val nat_iter : nat -> ('a1 -> 'a1) -> 'a1 -> 'a1
 
-val psize : positive -> nat
+type positive =
+| XI of positive
+| XO of positive
+| XH
 
 type n =
-  | N0
-  | Npos of positive
-
-val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1
+| N0
+| Npos of positive
 
 type z =
-  | Z0
-  | Zpos of positive
-  | Zneg of positive
-
-val zdouble_plus_one : z -> z
-
-val zdouble_minus_one : z -> z
-
-val zdouble : z -> z
-
-val zPminus : positive -> positive -> z
-
-val zplus : z -> z -> z
-
-val zopp : z -> z
-
-val zminus : z -> z -> z
-
-val zmult : z -> z -> z
-
-val zcompare : z -> z -> comparison
-
-val zabs : z -> z
+| Z0
+| Zpos of positive
+| Zneg of positive
+
+module type TotalOrder' = 
+ sig 
+  type t 
+ end
+
+module MakeOrderTac : 
+ functor (O:TotalOrder') ->
+ sig 
+  
+ end
+
+module MaxLogicalProperties : 
+ functor (O:TotalOrder') ->
+ functor (M:sig 
+  val max : O.t -> O.t -> O.t
+ end) ->
+ sig 
+  module T : 
+   sig 
+    
+   end
+ end
+
+module Pos : 
+ sig 
+  type t = positive
+  
+  val succ : positive -> positive
+  
+  val add : positive -> positive -> positive
+  
+  val add_carry : positive -> positive -> positive
+  
+  val pred_double : positive -> positive
+  
+  val pred : positive -> positive
+  
+  val pred_N : positive -> n
+  
+  type mask =
+  | IsNul
+  | IsPos of positive
+  | IsNeg
+  
+  val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1
+  
+  val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1
+  
+  val succ_double_mask : mask -> mask
+  
+  val double_mask : mask -> mask
+  
+  val double_pred_mask : positive -> mask
+  
+  val pred_mask : mask -> mask
+  
+  val sub_mask : positive -> positive -> mask
+  
+  val sub_mask_carry : positive -> positive -> mask
+  
+  val sub : positive -> positive -> positive
+  
+  val mul : positive -> positive -> positive
+  
+  val iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1
+  
+  val pow : positive -> positive -> positive
+  
+  val div2 : positive -> positive
+  
+  val div2_up : positive -> positive
+  
+  val size_nat : positive -> nat
+  
+  val size : positive -> positive
+  
+  val compare_cont : positive -> positive -> comparison -> comparison
+  
+  val compare : positive -> positive -> comparison
+  
+  val min : positive -> positive -> positive
+  
+  val max : positive -> positive -> positive
+  
+  val eqb : positive -> positive -> bool
+  
+  val leb : positive -> positive -> bool
+  
+  val ltb : positive -> positive -> bool
+  
+  val sqrtrem_step :
+    (positive -> positive) -> (positive -> positive) -> (positive * mask) ->
+    positive * mask
+  
+  val sqrtrem : positive -> positive * mask
+  
+  val sqrt : positive -> positive
+  
+  val gcdn : nat -> positive -> positive -> positive
+  
+  val gcd : positive -> positive -> positive
+  
+  val ggcdn : nat -> positive -> positive -> positive * (positive * positive)
+  
+  val ggcd : positive -> positive -> positive * (positive * positive)
+  
+  val coq_Nsucc_double : n -> n
+  
+  val coq_Ndouble : n -> n
+  
+  val coq_lor : positive -> positive -> positive
+  
+  val coq_land : positive -> positive -> n
+  
+  val ldiff : positive -> positive -> n
+  
+  val coq_lxor : positive -> positive -> n
+  
+  val shiftl_nat : positive -> nat -> positive
+  
+  val shiftr_nat : positive -> nat -> positive
+  
+  val shiftl : positive -> n -> positive
+  
+  val shiftr : positive -> n -> positive
+  
+  val testbit_nat : positive -> nat -> bool
+  
+  val testbit : positive -> n -> bool
+  
+  val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1
+  
+  val to_nat : positive -> nat
+  
+  val of_nat : nat -> positive
+  
+  val of_succ_nat : nat -> positive
+ end
+
+module Coq_Pos : 
+ sig 
+  module Coq__1 : sig 
+   type t = positive
+  end
+  type t = Coq__1.t
+  
+  val succ : positive -> positive
+  
+  val add : positive -> positive -> positive
+  
+  val add_carry : positive -> positive -> positive
+  
+  val pred_double : positive -> positive
+  
+  val pred : positive -> positive
+  
+  val pred_N : positive -> n
+  
+  type mask = Pos.mask =
+  | IsNul
+  | IsPos of positive
+  | IsNeg
+  
+  val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1
+  
+  val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1
+  
+  val succ_double_mask : mask -> mask
+  
+  val double_mask : mask -> mask
+  
+  val double_pred_mask : positive -> mask
+  
+  val pred_mask : mask -> mask
+  
+  val sub_mask : positive -> positive -> mask
+  
+  val sub_mask_carry : positive -> positive -> mask
+  
+  val sub : positive -> positive -> positive
+  
+  val mul : positive -> positive -> positive
+  
+  val iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1
+  
+  val pow : positive -> positive -> positive
+  
+  val div2 : positive -> positive
+  
+  val div2_up : positive -> positive
+  
+  val size_nat : positive -> nat
+  
+  val size : positive -> positive
+  
+  val compare_cont : positive -> positive -> comparison -> comparison
+  
+  val compare : positive -> positive -> comparison
+  
+  val min : positive -> positive -> positive
+  
+  val max : positive -> positive -> positive
+  
+  val eqb : positive -> positive -> bool
+  
+  val leb : positive -> positive -> bool
+  
+  val ltb : positive -> positive -> bool
+  
+  val sqrtrem_step :
+    (positive -> positive) -> (positive -> positive) -> (positive * mask) ->
+    positive * mask
+  
+  val sqrtrem : positive -> positive * mask
+  
+  val sqrt : positive -> positive
+  
+  val gcdn : nat -> positive -> positive -> positive
+  
+  val gcd : positive -> positive -> positive
+  
+  val ggcdn : nat -> positive -> positive -> positive * (positive * positive)
+  
+  val ggcd : positive -> positive -> positive * (positive * positive)
+  
+  val coq_Nsucc_double : n -> n
+  
+  val coq_Ndouble : n -> n
+  
+  val coq_lor : positive -> positive -> positive
+  
+  val coq_land : positive -> positive -> n
+  
+  val ldiff : positive -> positive -> n
+  
+  val coq_lxor : positive -> positive -> n
+  
+  val shiftl_nat : positive -> nat -> positive
+  
+  val shiftr_nat : positive -> nat -> positive
+  
+  val shiftl : positive -> n -> positive
+  
+  val shiftr : positive -> n -> positive
+  
+  val testbit_nat : positive -> nat -> bool
+  
+  val testbit : positive -> n -> bool
+  
+  val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1
+  
+  val to_nat : positive -> nat
+  
+  val of_nat : nat -> positive
+  
+  val of_succ_nat : nat -> positive
+  
+  val eq_dec : positive -> positive -> bool
+  
+  val peano_rect : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1
+  
+  val peano_rec : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1
+  
+  type coq_PeanoView =
+  | PeanoOne
+  | PeanoSucc of positive * coq_PeanoView
+  
+  val coq_PeanoView_rect :
+    'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive ->
+    coq_PeanoView -> 'a1
+  
+  val coq_PeanoView_rec :
+    'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive ->
+    coq_PeanoView -> 'a1
+  
+  val peanoView_xO : positive -> coq_PeanoView -> coq_PeanoView
+  
+  val peanoView_xI : positive -> coq_PeanoView -> coq_PeanoView
+  
+  val peanoView : positive -> coq_PeanoView
+  
+  val coq_PeanoView_iter :
+    'a1 -> (positive -> 'a1 -> 'a1) -> positive -> coq_PeanoView -> 'a1
+  
+  val switch_Eq : comparison -> comparison -> comparison
+  
+  val mask2cmp : mask -> comparison
+  
+  module T : 
+   sig 
+    
+   end
+  
+  module ORev : 
+   sig 
+    type t = Coq__1.t
+   end
+  
+  module MRev : 
+   sig 
+    val max : t -> t -> t
+   end
+  
+  module MPRev : 
+   sig 
+    module T : 
+     sig 
+      
+     end
+   end
+  
+  module P : 
+   sig 
+    val max_case_strong :
+      t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
+      'a1
+    
+    val max_case :
+      t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1
+    
+    val max_dec : t -> t -> bool
+    
+    val min_case_strong :
+      t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
+      'a1
+    
+    val min_case :
+      t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1
+    
+    val min_dec : t -> t -> bool
+   end
+  
+  val max_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
+  
+  val max_case : t -> t -> 'a1 -> 'a1 -> 'a1
+  
+  val max_dec : t -> t -> bool
+  
+  val min_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
+  
+  val min_case : t -> t -> 'a1 -> 'a1 -> 'a1
+  
+  val min_dec : t -> t -> bool
+ end
+
+module N : 
+ sig 
+  type t = n
+  
+  val zero : n
+  
+  val one : n
+  
+  val two : n
+  
+  val succ_double : n -> n
+  
+  val double : n -> n
+  
+  val succ : n -> n
+  
+  val pred : n -> n
+  
+  val succ_pos : n -> positive
+  
+  val add : n -> n -> n
+  
+  val sub : n -> n -> n
+  
+  val mul : n -> n -> n
+  
+  val compare : n -> n -> comparison
+  
+  val eqb : n -> n -> bool
+  
+  val leb : n -> n -> bool
+  
+  val ltb : n -> n -> bool
+  
+  val min : n -> n -> n
+  
+  val max : n -> n -> n
+  
+  val div2 : n -> n
+  
+  val even : n -> bool
+  
+  val odd : n -> bool
+  
+  val pow : n -> n -> n
+  
+  val log2 : n -> n
+  
+  val size : n -> n
+  
+  val size_nat : n -> nat
+  
+  val pos_div_eucl : positive -> n -> n * n
+  
+  val div_eucl : n -> n -> n * n
+  
+  val div : n -> n -> n
+  
+  val modulo : n -> n -> n
+  
+  val gcd : n -> n -> n
+  
+  val ggcd : n -> n -> n * (n * n)
+  
+  val sqrtrem : n -> n * n
+  
+  val sqrt : n -> n
+  
+  val coq_lor : n -> n -> n
+  
+  val coq_land : n -> n -> n
+  
+  val ldiff : n -> n -> n
+  
+  val coq_lxor : n -> n -> n
+  
+  val shiftl_nat : n -> nat -> n
+  
+  val shiftr_nat : n -> nat -> n
+  
+  val shiftl : n -> n -> n
+  
+  val shiftr : n -> n -> n
+  
+  val testbit_nat : n -> nat -> bool
+  
+  val testbit : n -> n -> bool
+  
+  val to_nat : n -> nat
+  
+  val of_nat : nat -> n
+  
+  val iter : n -> ('a1 -> 'a1) -> 'a1 -> 'a1
+  
+  val eq_dec : n -> n -> bool
+  
+  val discr : n -> positive option
+  
+  val binary_rect : 'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1
+  
+  val binary_rec : 'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1
+  
+  val peano_rect : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1
+  
+  val peano_rec : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1
+  
+  module BootStrap : 
+   sig 
+    
+   end
+  
+  val recursion : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1
+  
+  module OrderElts : 
+   sig 
+    type t = n
+   end
+  
+  module OrderTac : 
+   sig 
+    
+   end
+  
+  module NZPowP : 
+   sig 
+    
+   end
+  
+  module NZSqrtP : 
+   sig 
+    
+   end
+  
+  val sqrt_up : n -> n
+  
+  val log2_up : n -> n
+  
+  module NZDivP : 
+   sig 
+    
+   end
+  
+  val lcm : n -> n -> n
+  
+  val b2n : bool -> n
+  
+  val setbit : n -> n -> n
+  
+  val clearbit : n -> n -> n
+  
+  val ones : n -> n
+  
+  val lnot : n -> n -> n
+  
+  module T : 
+   sig 
+    
+   end
+  
+  module ORev : 
+   sig 
+    type t = n
+   end
+  
+  module MRev : 
+   sig 
+    val max : n -> n -> n
+   end
+  
+  module MPRev : 
+   sig 
+    module T : 
+     sig 
+      
+     end
+   end
+  
+  module P : 
+   sig 
+    val max_case_strong :
+      n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
+      'a1
+    
+    val max_case :
+      n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1
+    
+    val max_dec : n -> n -> bool
+    
+    val min_case_strong :
+      n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
+      'a1
+    
+    val min_case :
+      n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1
+    
+    val min_dec : n -> n -> bool
+   end
+  
+  val max_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
+  
+  val max_case : n -> n -> 'a1 -> 'a1 -> 'a1
+  
+  val max_dec : n -> n -> bool
+  
+  val min_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
+  
+  val min_case : n -> n -> 'a1 -> 'a1 -> 'a1
+  
+  val min_dec : n -> n -> bool
+ end
 
-val zmax : z -> z -> z
+val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1
 
-val zle_bool : z -> z -> bool
+val nth : nat -> 'a1 list -> 'a1 -> 'a1
 
-val zge_bool : z -> z -> bool
+val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
 
-val zgt_bool : z -> z -> bool
+val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1
+
+module Z : 
+ sig 
+  type t = z
+  
+  val zero : z
+  
+  val one : z
+  
+  val two : z
+  
+  val double : z -> z
+  
+  val succ_double : z -> z
+  
+  val pred_double : z -> z
+  
+  val pos_sub : positive -> positive -> z
+  
+  val add : z -> z -> z
+  
+  val opp : z -> z
+  
+  val succ : z -> z
+  
+  val pred : z -> z
+  
+  val sub : z -> z -> z
+  
+  val mul : z -> z -> z
+  
+  val pow_pos : z -> positive -> z
+  
+  val pow : z -> z -> z
+  
+  val compare : z -> z -> comparison
+  
+  val sgn : z -> z
+  
+  val leb : z -> z -> bool
+  
+  val geb : z -> z -> bool
+  
+  val ltb : z -> z -> bool
+  
+  val gtb : z -> z -> bool
+  
+  val eqb : z -> z -> bool
+  
+  val max : z -> z -> z
+  
+  val min : z -> z -> z
+  
+  val abs : z -> z
+  
+  val abs_nat : z -> nat
+  
+  val abs_N : z -> n
+  
+  val to_nat : z -> nat
+  
+  val to_N : z -> n
+  
+  val of_nat : nat -> z
+  
+  val of_N : n -> z
+  
+  val iter : z -> ('a1 -> 'a1) -> 'a1 -> 'a1
+  
+  val pos_div_eucl : positive -> z -> z * z
+  
+  val div_eucl : z -> z -> z * z
+  
+  val div : z -> z -> z
+  
+  val modulo : z -> z -> z
+  
+  val quotrem : z -> z -> z * z
+  
+  val quot : z -> z -> z
+  
+  val rem : z -> z -> z
+  
+  val even : z -> bool
+  
+  val odd : z -> bool
+  
+  val div2 : z -> z
+  
+  val quot2 : z -> z
+  
+  val log2 : z -> z
+  
+  val sqrtrem : z -> z * z
+  
+  val sqrt : z -> z
+  
+  val gcd : z -> z -> z
+  
+  val ggcd : z -> z -> z * (z * z)
+  
+  val testbit : z -> z -> bool
+  
+  val shiftl : z -> z -> z
+  
+  val shiftr : z -> z -> z
+  
+  val coq_lor : z -> z -> z
+  
+  val coq_land : z -> z -> z
+  
+  val ldiff : z -> z -> z
+  
+  val coq_lxor : z -> z -> z
+  
+  val eq_dec : z -> z -> bool
+  
+  module BootStrap : 
+   sig 
+    
+   end
+  
+  module OrderElts : 
+   sig 
+    type t = z
+   end
+  
+  module OrderTac : 
+   sig 
+    
+   end
+  
+  val sqrt_up : z -> z
+  
+  val log2_up : z -> z
+  
+  module NZDivP : 
+   sig 
+    
+   end
+  
+  module Quot2Div : 
+   sig 
+    val div : z -> z -> z
+    
+    val modulo : z -> z -> z
+   end
+  
+  module NZQuot : 
+   sig 
+    
+   end
+  
+  val lcm : z -> z -> z
+  
+  val b2z : bool -> z
+  
+  val setbit : z -> z -> z
+  
+  val clearbit : z -> z -> z
+  
+  val lnot : z -> z
+  
+  val ones : z -> z
+  
+  module T : 
+   sig 
+    
+   end
+  
+  module ORev : 
+   sig 
+    type t = z
+   end
+  
+  module MRev : 
+   sig 
+    val max : z -> z -> z
+   end
+  
+  module MPRev : 
+   sig 
+    module T : 
+     sig 
+      
+     end
+   end
+  
+  module P : 
+   sig 
+    val max_case_strong :
+      z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
+      'a1
+    
+    val max_case :
+      z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1
+    
+    val max_dec : z -> z -> bool
+    
+    val min_case_strong :
+      z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
+      'a1
+    
+    val min_case :
+      z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1
+    
+    val min_dec : z -> z -> bool
+   end
+  
+  val max_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
+  
+  val max_case : z -> z -> 'a1 -> 'a1 -> 'a1
+  
+  val max_dec : z -> z -> bool
+  
+  val min_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
+  
+  val min_case : z -> z -> 'a1 -> 'a1 -> 'a1
+  
+  val min_dec : z -> z -> bool
+ end
 
 val zeq_bool : z -> z -> bool
 
-val n_of_nat : nat -> n
-
-val zdiv_eucl_POS : positive -> z -> z  *  z
-
-val zdiv_eucl : z -> z -> z  *  z
-
-val zdiv : z -> z -> z
-
 type 'c pol =
-  | Pc of 'c
-  | Pinj of positive * 'c pol
-  | PX of 'c pol * positive * 'c pol
+| Pc of 'c
+| Pinj of positive * 'c pol
+| PX of 'c pol * positive * 'c pol
 
 val p0 : 'a1 -> 'a1 pol
 
@@ -117,6 +850,8 @@ 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 :
@@ -177,13 +912,13 @@ val psquare :
   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
+| 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
 
@@ -200,14 +935,16 @@ val norm_aux :
   '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
+| 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 'term' clause = 'term' list
 
@@ -217,41 +954,65 @@ val tt : 'a1 cnf
 
 val ff : 'a1 cnf
 
-val or_clause_cnf : 'a1 clause -> 'a1 cnf -> 'a1 cnf
+val add_term :
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> 'a1
+  clause option
 
-val or_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf
+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 :
-  ('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 ->
+  'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf
 
 val cnf_checker : ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool
 
 val tauto_checker :
-  ('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1
-  bFormula -> 'a3 list -> bool
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 ->
+  'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 list -> bool
+
+val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
+
+val cltb : ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
 
 type 'c polC = 'c pol
 
 type op1 =
-  | Equal
-  | NonEqual
-  | Strict
-  | NonStrict
+| Equal
+| NonEqual
+| Strict
+| NonStrict
+
+type 'c nFormula = 'c polC * op1
 
-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
+| 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 ->
@@ -278,14 +1039,14 @@ val check_normalised_formulas :
   bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool
 
 type op2 =
-  | OpEq
-  | OpNEq
-  | OpLe
-  | OpGe
-  | OpLt
-  | OpGt
+| OpEq
+| OpNEq
+| OpLe
+| OpGe
+| OpLt
+| OpGt
 
-type 'c formula = { flhs : 'c pExpr; fop : op2; frhs : 'c pExpr }
+type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr }
 
 val flhs : 'a1 formula -> 'a1 pExpr
 
@@ -329,6 +1090,10 @@ 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
@@ -357,18 +1122,12 @@ val qpower_positive : q -> positive -> q
 
 val qpower : q -> z -> q
 
-val pgcdn : nat -> positive -> positive -> positive
-
-val pgcd : positive -> positive -> positive
-
-val zgcd : z -> z -> z
-
-type 'a t =
-  | Empty
-  | Leaf of 'a
-  | Node of 'a t * 'a * 'a t
+type 'a t0 =
+| Empty
+| Leaf of 'a
+| Node of 'a t0 * 'a * 'a t0
 
-val find : 'a1 -> 'a1 t -> positive -> 'a1
+val find : 'a1 -> 'a1 t0 -> positive -> 'a1
 
 type zWitness = z psatz
 
@@ -388,38 +1147,40 @@ 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
+| 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 zgcd_pol : z polC -> z * z
 
 val zdiv_pol : z polC -> z -> z polC
 
-val makeCuttingPlane : z polC -> z polC  *  z
+val makeCuttingPlane : z polC -> z polC * z
 
-val genCuttingPlane : z nFormula -> ((z polC  *  z)  *  op1) option
+val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option
 
-val nformula_of_cutting_plane : ((z polC  *  z)  *  op1) -> z nFormula
+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 check_inconsistent0 : z nFormula -> bool
+val valid_cut_sign : op1 -> bool
 
 val zChecker : z nFormula list -> zArithProof -> bool
 
 val zTautoChecker : z formula bFormula -> zArithProof list -> bool
 
-val n_of_Z : z -> n
-
 type qWitness = q psatz
 
 val qWeakChecker : q nFormula list -> q psatz -> bool
@@ -428,15 +1189,36 @@ 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 rWitness = z psatz
+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 rWeakChecker : z nFormula list -> z psatz -> bool
+val rnegate : q formula -> q nFormula cnf
 
-val rnormalise : z formula -> z nFormula cnf
+val runsat : q nFormula -> bool
 
-val rnegate : z formula -> z nFormula cnf
+val rdeduce : q nFormula -> q nFormula -> q nFormula option
 
-val rTautoChecker : z formula bFormula -> rWitness list -> bool
+val rTautoChecker : rcst formula bFormula -> rWitness list -> bool