added support to handle division by a constant over R

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

1 files changed, 833 insertions, 91 deletions

diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 675a5a0cc..bcd61f39b 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -1,9 +1,17 @@
+type __ = Obj.t
+
 val negb : bool -> bool
 
 type nat =
 | O
 | S of nat
 
+val fst : ('a1 * 'a2) -> 'a1
+
+val snd : ('a1 * 'a2) -> 'a2
+
+val app : 'a1 list -> 'a1 list -> 'a1 list
+
 type comparison =
 | Eq
 | Lt
@@ -11,109 +19,826 @@ type comparison =
 
 val compOpp : comparison -> comparison
 
-val app : 'a1 list -> 'a1 list -> 'a1 list
-
-val plus : nat -> nat -> nat
-
-type positive =
-| XI of positive
-| XO of positive
-| XH
-
-val psucc : positive -> positive
-
-val pplus : positive -> positive -> positive
+type compareSpecT =
+| CompEqT
+| CompLtT
+| CompGtT
 
-val pplus_carry : positive -> positive -> positive
+val compareSpec2Type : comparison -> compareSpecT
 
-val p_of_succ_nat : nat -> positive
+type 'a compSpecT = compareSpecT
 
-val pdouble_minus_one : positive -> positive
+val compSpec2Type : 'a1 -> 'a1 -> comparison -> 'a1 compSpecT
 
-type positive_mask =
-| IsNul
-| IsPos of positive
-| IsNeg
+type 'a sig0 =
+  'a
+  (* singleton inductive, whose constructor was exist *)
 
-val pdouble_plus_one_mask : positive_mask -> positive_mask
-
-val pdouble_mask : positive_mask -> positive_mask
-
-val pdouble_minus_two : positive -> positive_mask
-
-val pminus_mask : positive -> positive -> positive_mask
-
-val pminus_mask_carry : positive -> positive -> positive_mask
-
-val pminus : positive -> positive -> positive
-
-val pmult : positive -> positive -> positive
+val plus : nat -> nat -> nat
 
-val psize : positive -> nat
+val nat_iter : nat -> ('a1 -> 'a1) -> 'a1 -> 'a1
 
-val pcompare : positive -> positive -> comparison -> comparison
+type positive =
+| XI of positive
+| XO of positive
+| XH
 
 type n =
 | N0
 | Npos of positive
 
-val n_of_nat : nat -> n
-
-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
-
 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
+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 zplus : z -> z -> z
-
-val zopp : z -> z
-
-val zminus : z -> z -> z
-
-val zmult : z -> z -> z
-
-val zcompare : z -> z -> comparison
-
-val zmax : z -> z -> z
+val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1
 
-val zabs : z -> z
+val nth : nat -> 'a1 list -> 'a1 -> 'a1
 
-val zle_bool : z -> z -> bool
+val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
 
-val zge_bool : z -> z -> bool
+val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1
 
-val zgt_bool : z -> z -> bool
+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 pgcdn : nat -> positive -> positive -> positive
-
-val pgcd : positive -> positive -> positive
-
-val zgcd : z -> z -> z
-
-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
@@ -219,6 +944,8 @@ type '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
 
 type 'term' cnf = 'term' clause list
@@ -319,7 +1046,7 @@ type op2 =
 | 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
 
@@ -363,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
@@ -391,12 +1122,12 @@ val qpower_positive : q -> positive -> q
 
 val qpower : q -> z -> q
 
-type 'a t =
+type 'a t0 =
 | Empty
 | Leaf of 'a
-| Node of 'a t * 'a * 'a t
+| 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
 
@@ -450,8 +1181,6 @@ 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
@@ -466,17 +1195,30 @@ 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 : z nFormula list -> z psatz -> bool
+val rWeakChecker : q nFormula list -> q psatz -> bool
 
-val rnormalise : z formula -> z nFormula cnf
+val rnormalise : q formula -> q nFormula cnf
 
-val rnegate : z formula -> z nFormula cnf
+val rnegate : q formula -> q nFormula cnf
 
-val runsat : z nFormula -> bool
+val runsat : q nFormula -> bool
 
-val rdeduce : z nFormula -> z nFormula -> z nFormula option
+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