[micromega] native support for boolean operators

The syntax of formulae is extended to support boolean constants (true,
false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb,
Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and
Z.ltb.

4 files changed, 1081 insertions, 423 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 0f8d941b41..44bc20e55f 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -86,20 +86,30 @@ type 'cst formula =
 type 'cst clause = ('cst Mc.nFormula, tag * EConstr.constr) Mc.clause
 type 'cst cnf = ('cst Mc.nFormula, tag * EConstr.constr) Mc.cnf
 
+let pp_kind o = function
+  | Mc.IsProp -> output_string o "Prop"
+  | Mc.IsBool -> output_string o "bool"
+
+let kind_is_prop = function Mc.IsProp -> true | Mc.IsBool -> false
+
 let rec pp_formula o (f : 'cst formula) =
   Mc.(
     match f with
-    | TT -> output_string o "tt"
-    | FF -> output_string o "ff"
-    | X c -> output_string o "X "
-    | A (_, (t, _)) -> Printf.fprintf o "A(%a)" Tag.pp t
-    | Cj (f1, f2) -> Printf.fprintf o "C(%a,%a)" pp_formula f1 pp_formula f2
-    | D (f1, f2) -> Printf.fprintf o "D(%a,%a)" pp_formula f1 pp_formula f2
-    | I (f1, n, f2) ->
-      Printf.fprintf o "I(%a,%s,%a)" pp_formula f1
+    | TT k -> output_string o (if kind_is_prop k then "True" else "true")
+    | FF k -> output_string o (if kind_is_prop k then "False" else "false")
+    | X (k, c) -> Printf.fprintf o "X %a" pp_kind k
+    | A (_, _, (t, _)) -> Printf.fprintf o "A(%a)" Tag.pp t
+    | AND (_, f1, f2) ->
+      Printf.fprintf o "AND(%a,%a)" pp_formula f1 pp_formula f2
+    | OR (_, f1, f2) -> Printf.fprintf o "OR(%a,%a)" pp_formula f1 pp_formula f2
+    | IMPL (_, f1, n, f2) ->
+      Printf.fprintf o "IMPL(%a,%s,%a)" pp_formula f1
         (match n with Some id -> Names.Id.to_string id | None -> "")
         pp_formula f2
-    | N f -> Printf.fprintf o "N(%a)" pp_formula f)
+    | NOT (_, f) -> Printf.fprintf o "NOT(%a)" pp_formula f
+    | IFF (_, f1, f2) ->
+      Printf.fprintf o "IFF(%a,%a)" pp_formula f1 pp_formula f2
+    | EQ (f1, f2) -> Printf.fprintf o "EQ(%a,%a)" pp_formula f1 pp_formula f2)
 
 (**
   * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of
@@ -142,6 +152,14 @@ module M = struct
   let coq_iff = lazy (constr_of_ref "core.iff.type")
   let coq_True = lazy (constr_of_ref "core.True.type")
   let coq_False = lazy (constr_of_ref "core.False.type")
+  let coq_bool = lazy (constr_of_ref "core.bool.type")
+  let coq_true = lazy (constr_of_ref "core.bool.true")
+  let coq_false = lazy (constr_of_ref "core.bool.false")
+  let coq_andb = lazy (constr_of_ref "core.bool.andb")
+  let coq_orb = lazy (constr_of_ref "core.bool.orb")
+  let coq_implb = lazy (constr_of_ref "core.bool.implb")
+  let coq_eqb = lazy (constr_of_ref "core.bool.eqb")
+  let coq_negb = lazy (constr_of_ref "core.bool.negb")
   let coq_cons = lazy (constr_of_ref "core.list.cons")
   let coq_nil = lazy (constr_of_ref "core.list.nil")
   let coq_list = lazy (constr_of_ref "core.list.type")
@@ -186,11 +204,18 @@ module M = struct
   let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof")
   let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof")
   let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof")
+  let coq_IsProp = lazy (constr_of_ref "micromega.kind.isProp")
+  let coq_IsBool = lazy (constr_of_ref "micromega.kind.isBool")
   let coq_Zgt = lazy (constr_of_ref "num.Z.gt")
   let coq_Zge = lazy (constr_of_ref "num.Z.ge")
   let coq_Zle = lazy (constr_of_ref "num.Z.le")
   let coq_Zlt = lazy (constr_of_ref "num.Z.lt")
-  let coq_Eq = lazy (constr_of_ref "core.eq.type")
+  let coq_Zgtb = lazy (constr_of_ref "num.Z.gtb")
+  let coq_Zgeb = lazy (constr_of_ref "num.Z.geb")
+  let coq_Zleb = lazy (constr_of_ref "num.Z.leb")
+  let coq_Zltb = lazy (constr_of_ref "num.Z.ltb")
+  let coq_Zeqb = lazy (constr_of_ref "num.Z.eqb")
+  let coq_eq = lazy (constr_of_ref "core.eq.type")
   let coq_Zplus = lazy (constr_of_ref "num.Z.add")
   let coq_Zminus = lazy (constr_of_ref "num.Z.sub")
   let coq_Zopp = lazy (constr_of_ref "num.Z.opp")
@@ -248,13 +273,16 @@ module M = struct
 
   let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT")
   let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF")
-  let coq_And = lazy (constr_of_ref "micromega.GFormula.Cj")
-  let coq_Or = lazy (constr_of_ref "micromega.GFormula.D")
-  let coq_Neg = lazy (constr_of_ref "micromega.GFormula.N")
+  let coq_AND = lazy (constr_of_ref "micromega.GFormula.AND")
+  let coq_OR = lazy (constr_of_ref "micromega.GFormula.OR")
+  let coq_NOT = lazy (constr_of_ref "micromega.GFormula.NOT")
   let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A")
   let coq_X = lazy (constr_of_ref "micromega.GFormula.X")
-  let coq_Impl = lazy (constr_of_ref "micromega.GFormula.I")
+  let coq_IMPL = lazy (constr_of_ref "micromega.GFormula.IMPL")
+  let coq_IFF = lazy (constr_of_ref "micromega.GFormula.IFF")
+  let coq_EQ = lazy (constr_of_ref "micromega.GFormula.EQ")
   let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type")
+  let coq_eKind = lazy (constr_of_ref "micromega.eKind")
 
   (**
     * Initialization : a few Caml symbols are derived from other libraries;
@@ -557,52 +585,56 @@ module M = struct
         (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l)
     with Not_found -> raise ParseError
 
-  let zop_table =
+  let zop_table_prop =
     [ (coq_Zgt, Mc.OpGt)
     ; (coq_Zge, Mc.OpGe)
     ; (coq_Zlt, Mc.OpLt)
     ; (coq_Zle, Mc.OpLe) ]
 
-  let rop_table =
+  let zop_table_bool =
+    [ (coq_Zgtb, Mc.OpGt)
+    ; (coq_Zgeb, Mc.OpGe)
+    ; (coq_Zltb, Mc.OpLt)
+    ; (coq_Zleb, Mc.OpLe)
+    ; (coq_Zeqb, Mc.OpEq) ]
+
+  let rop_table_prop =
     [ (coq_Rgt, Mc.OpGt)
     ; (coq_Rge, Mc.OpGe)
     ; (coq_Rlt, Mc.OpLt)
     ; (coq_Rle, Mc.OpLe) ]
 
-  let qop_table = [(coq_Qlt, Mc.OpLt); (coq_Qle, Mc.OpLe); (coq_Qeq, Mc.OpEq)]
+  let rop_table_bool = []
+
+  let qop_table_prop =
+    [(coq_Qlt, Mc.OpLt); (coq_Qle, Mc.OpLe); (coq_Qeq, Mc.OpEq)]
+
+  let qop_table_bool = []
 
   type gl = {env : Environ.env; sigma : Evd.evar_map}
 
   let is_convertible gl t1 t2 = Reductionops.is_conv gl.env gl.sigma t1 t2
 
-  let parse_zop gl (op, args) =
+  let parse_operator table_prop table_bool has_equality typ gl k (op, args) =
     let sigma = gl.sigma in
     match args with
-    | [|a1; a2|] -> (assoc_const sigma op zop_table, a1, a2)
+    | [|a1; a2|] ->
+      ( assoc_const sigma op
+          (match k with Mc.IsProp -> table_prop | Mc.IsBool -> table_bool)
+      , a1
+      , a2 )
     | [|ty; a1; a2|] ->
       if
-        EConstr.eq_constr sigma op (Lazy.force coq_Eq)
-        && is_convertible gl ty (Lazy.force coq_Z)
+        has_equality
+        && EConstr.eq_constr sigma op (Lazy.force coq_eq)
+        && is_convertible gl ty (Lazy.force typ)
       then (Mc.OpEq, args.(1), args.(2))
       else raise ParseError
     | _ -> raise ParseError
 
-  let parse_rop gl (op, args) =
-    let sigma = gl.sigma in
-    match args with
-    | [|a1; a2|] -> (assoc_const sigma op rop_table, a1, a2)
-    | [|ty; a1; a2|] ->
-      if
-        EConstr.eq_constr sigma op (Lazy.force coq_Eq)
-        && is_convertible gl ty (Lazy.force coq_R)
-      then (Mc.OpEq, a1, a2)
-      else raise ParseError
-    | _ -> raise ParseError
-
-  let parse_qop gl (op, args) =
-    if Array.length args = 2 then
-      (assoc_const gl.sigma op qop_table, args.(0), args.(1))
-    else raise ParseError
+  let parse_zop = parse_operator zop_table_prop zop_table_bool true coq_Z
+  let parse_rop = parse_operator rop_table_prop [] true coq_R
+  let parse_qop = parse_operator qop_table_prop [] false coq_R
 
   type 'a op =
     | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr)
@@ -622,7 +654,7 @@ module M = struct
 
   module Env = struct
     type t =
-      { vars : EConstr.t list
+      { vars : (EConstr.t * Mc.kind) list
       ; (* The list represents a mapping from EConstr.t to indexes. *)
         gl : gl
             (* The evar_map may be updated due to unification of universes *) }
@@ -642,16 +674,16 @@ module M = struct
         | exception Univ.UniverseInconsistency _ -> None )
       | None -> None
 
-    let compute_rank_add env v =
+    let compute_rank_add env v is_prop =
       let rec _add gl vars n v =
         match vars with
-        | [] -> (gl, [v], n)
-        | e :: l -> (
+        | [] -> (gl, [(v, is_prop)], n)
+        | (e, b) :: l -> (
           match eq_constr gl e v with
           | Some gl' -> (gl', vars, n)
           | None ->
             let gl, l', n = _add gl l (n + 1) v in
-            (gl, e :: l', n) )
+            (gl, (e, b) :: l', n) )
       in
       let gl', vars', n = _add env.gl env.vars 1 v in
       ({vars = vars'; gl = gl'}, CamlToCoq.positive n)
@@ -661,7 +693,7 @@ module M = struct
       let rec _get_rank env n =
         match env with
         | [] -> raise (Invalid_argument "get_rank")
-        | e :: l -> (
+        | (e, _) :: l -> (
           match eq_constr gl e v with Some _ -> n | None -> _get_rank l (n + 1)
           )
       in
@@ -682,7 +714,7 @@ module M = struct
     let pp gl env =
       let ppl =
         List.mapi
-          (fun i e ->
+          (fun i (e, _) ->
             Pp.str "x"
             ++ Pp.int (i + 1)
             ++ Pp.str ":"
@@ -703,7 +735,7 @@ module M = struct
       Feedback.msg_debug
         (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env gl.env gl.sigma term);
     let parse_variable env term =
-      let env, n = Env.compute_rank_add env term in
+      let env, n = Env.compute_rank_add env term Mc.IsBool in
       (Mc.PEX n, env)
     in
     let rec parse_expr env term =
@@ -730,13 +762,13 @@ module M = struct
                 (power, env)
               with ParseError ->
                 (* if the exponent is a variable *)
-                let env, n = Env.compute_rank_add env term in
+                let env, n = Env.compute_rank_add env term Mc.IsBool in
                 (Mc.PEX n, env) )
             | Ukn s ->
               if debug then (
                 Printf.printf "unknown op: %s\n" s;
                 flush stdout );
-              let env, n = Env.compute_rank_add env term in
+              let env, n = Env.compute_rank_add env term Mc.IsBool in
               (Mc.PEX n, env) )
           | _ -> parse_variable env term )
         | _ -> parse_variable env term )
@@ -878,7 +910,7 @@ module M = struct
         Mc.PEpow (expr, exp))
       rop_spec
 
-  let parse_arith parse_op parse_expr env cstr gl =
+  let parse_arith parse_op parse_expr (k : Mc.kind) env cstr gl =
     let sigma = gl.sigma in
     if debug then
       Feedback.msg_debug
@@ -887,7 +919,7 @@ module M = struct
         ++ fnl () );
     match EConstr.kind sigma cstr with
     | App (op, args) ->
-      let op, lhs, rhs = parse_op gl (op, args) in
+      let op, lhs, rhs = parse_op gl k (op, args) in
       let e1, env = parse_expr gl env lhs in
       let e2, env = parse_expr gl env rhs in
       ({Mc.flhs = e1; Mc.fop = op; Mc.frhs = e2}, env)
@@ -899,13 +931,16 @@ module M = struct
 
   (* generic parsing of arithmetic expressions *)
 
-  let mkC f1 f2 = Mc.Cj (f1, f2)
-  let mkD f1 f2 = Mc.D (f1, f2)
-  let mkIff f1 f2 = Mc.Cj (Mc.I (f1, None, f2), Mc.I (f2, None, f1))
-  let mkI f1 f2 = Mc.I (f1, None, f2)
+  let mkAND b f1 f2 = Mc.AND (b, f1, f2)
+  let mkOR b f1 f2 = Mc.OR (b, f1, f2)
+  let mkIff b f1 f2 = Mc.IFF (b, f1, f2)
+  let mkIMPL b f1 f2 = Mc.IMPL (b, f1, None, f2)
+  let mkEQ f1 f2 = Mc.EQ (f1, f2)
 
-  let mkformula_binary g term f1 f2 =
-    match (f1, f2) with Mc.X _, Mc.X _ -> Mc.X term | _ -> g f1 f2
+  let mkformula_binary b g term f1 f2 =
+    match (f1, f2) with
+    | Mc.X (b1, _), Mc.X (b2, _) -> Mc.X (b, term)
+    | _ -> g f1 f2
 
   (**
     * This is the big generic function for formula parsers.
@@ -915,83 +950,129 @@ module M = struct
     let sort = Retyping.get_sort_of env sigma term in
     Sorts.is_prop sort
 
+  type formula_op =
+    { op_and : EConstr.t
+    ; op_or : EConstr.t
+    ; op_iff : EConstr.t
+    ; op_not : EConstr.t
+    ; op_tt : EConstr.t
+    ; op_ff : EConstr.t }
+
+  let prop_op =
+    lazy
+      { op_and = Lazy.force coq_and
+      ; op_or = Lazy.force coq_or
+      ; op_iff = Lazy.force coq_iff
+      ; op_not = Lazy.force coq_not
+      ; op_tt = Lazy.force coq_True
+      ; op_ff = Lazy.force coq_False }
+
+  let bool_op =
+    lazy
+      { op_and = Lazy.force coq_andb
+      ; op_or = Lazy.force coq_orb
+      ; op_iff = Lazy.force coq_eqb
+      ; op_not = Lazy.force coq_negb
+      ; op_tt = Lazy.force coq_true
+      ; op_ff = Lazy.force coq_false }
+
   let parse_formula gl parse_atom env tg term =
     let sigma = gl.sigma in
-    let is_prop term = is_prop gl.env gl.sigma term in
-    let parse_atom env tg t =
+    let parse_atom b env tg t =
       try
-        let at, env = parse_atom env t gl in
-        (Mc.A (at, (tg, t)), env, Tag.next tg)
-      with ParseError ->
-        if is_prop t then (Mc.X t, env, tg) else raise ParseError
+        let at, env = parse_atom b env t gl in
+        (Mc.A (b, at, (tg, t)), env, Tag.next tg)
+      with ParseError -> (Mc.X (b, t), env, tg)
     in
-    let rec xparse_formula env tg term =
+    let prop_op = Lazy.force prop_op in
+    let bool_op = Lazy.force bool_op in
+    let eq = Lazy.force coq_eq in
+    let bool = Lazy.force coq_bool in
+    let rec xparse_formula op k env tg term =
       match EConstr.kind sigma term with
       | App (l, rst) -> (
         match rst with
-        | [|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 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 EConstr.eq_constr sigma l (Lazy.force coq_not) ->
-          let f, env, tg = xparse_formula env tg a in
-          (Mc.N f, env, tg)
-        | [|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 )
+        | [|a; b|] when EConstr.eq_constr sigma l op.op_and ->
+          let f, env, tg = xparse_formula op k env tg a in
+          let g, env, tg = xparse_formula op k env tg b in
+          (mkformula_binary k (mkAND k) term f g, env, tg)
+        | [|a; b|] when EConstr.eq_constr sigma l op.op_or ->
+          let f, env, tg = xparse_formula op k env tg a in
+          let g, env, tg = xparse_formula op k env tg b in
+          (mkformula_binary k (mkOR k) term f g, env, tg)
+        | [|a; b|] when EConstr.eq_constr sigma l op.op_iff ->
+          let f, env, tg = xparse_formula op k env tg a in
+          let g, env, tg = xparse_formula op k env tg b in
+          (mkformula_binary k (mkIff k) term f g, env, tg)
+        | [|ty; a; b|]
+          when EConstr.eq_constr sigma l eq && is_convertible gl ty bool ->
+          let f, env, tg = xparse_formula bool_op Mc.IsBool env tg a in
+          let g, env, tg = xparse_formula bool_op Mc.IsBool env tg b in
+          (mkformula_binary Mc.IsProp mkEQ term f g, env, tg)
+        | [|a|] when EConstr.eq_constr sigma l op.op_not ->
+          let f, env, tg = xparse_formula op k env tg a in
+          (Mc.NOT (k, f), env, tg)
+        | _ -> parse_atom k env tg term )
       | Prod (typ, a, b)
-        when typ.binder_name = Anonymous || 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 kind_is_prop k
+             && (typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b)
+        ->
+        let f, env, tg = xparse_formula op k env tg a in
+        let g, env, tg = xparse_formula op k env tg b in
+        (mkformula_binary Mc.IsProp (mkIMPL Mc.IsProp) term f g, env, tg)
       | _ ->
-        if EConstr.eq_constr sigma term (Lazy.force coq_True) then
-          (Mc.TT, env, tg)
-        else if EConstr.eq_constr sigma term (Lazy.force coq_False) then
-          Mc.(FF, env, tg)
-        else if is_prop term then (Mc.X term, env, tg)
-        else raise ParseError
+        if EConstr.eq_constr sigma term op.op_tt then (Mc.TT k, env, tg)
+        else if EConstr.eq_constr sigma term op.op_ff then Mc.(FF k, env, tg)
+        else (Mc.X (k, term), env, tg)
     in
-    xparse_formula env tg (*Reductionops.whd_zeta*) term
+    xparse_formula prop_op Mc.IsProp env tg (*Reductionops.whd_zeta*) term
+
+  (*  let dump_bool b = Lazy.force (if b then coq_true else coq_false)*)
+
+  let dump_kind k =
+    Lazy.force (match k with Mc.IsProp -> coq_IsProp | Mc.IsBool -> coq_IsBool)
 
   let dump_formula typ dump_atom f =
     let app_ctor c args =
       EConstr.mkApp
         ( Lazy.force c
         , Array.of_list
-            ( typ :: EConstr.mkProp :: Lazy.force coq_unit
+            ( typ :: Lazy.force coq_eKind :: Lazy.force coq_unit
             :: Lazy.force coq_unit :: args ) )
     in
     let rec xdump f =
       match f with
-      | Mc.TT -> app_ctor coq_TT []
-      | Mc.FF -> app_ctor coq_FF []
-      | Mc.Cj (x, y) -> app_ctor coq_And [xdump x; xdump y]
-      | Mc.D (x, y) -> app_ctor coq_Or [xdump x; xdump y]
-      | Mc.I (x, _, y) ->
-        app_ctor coq_Impl
-          [ xdump x
+      | Mc.TT k -> app_ctor coq_TT [dump_kind k]
+      | Mc.FF k -> app_ctor coq_FF [dump_kind k]
+      | Mc.AND (k, x, y) -> app_ctor coq_AND [dump_kind k; xdump x; xdump y]
+      | Mc.OR (k, x, y) -> app_ctor coq_OR [dump_kind k; xdump x; xdump y]
+      | Mc.IMPL (k, x, _, y) ->
+        app_ctor coq_IMPL
+          [ dump_kind k
+          ; xdump x
           ; EConstr.mkApp (Lazy.force coq_None, [|Lazy.force coq_unit|])
           ; xdump y ]
-      | Mc.N x -> app_ctor coq_Neg [xdump x]
-      | Mc.A (x, _) -> app_ctor coq_Atom [dump_atom x; Lazy.force coq_tt]
-      | Mc.X t -> app_ctor coq_X [t]
+      | Mc.NOT (k, x) -> app_ctor coq_NOT [dump_kind k; xdump x]
+      | Mc.IFF (k, x, y) -> app_ctor coq_IFF [dump_kind k; xdump x; xdump y]
+      | Mc.EQ (x, y) -> app_ctor coq_EQ [xdump x; xdump y]
+      | Mc.A (k, x, _) ->
+        app_ctor coq_Atom [dump_kind k; dump_atom x; Lazy.force coq_tt]
+      | Mc.X (k, t) -> app_ctor coq_X [dump_kind k; t]
     in
     xdump f
 
   let prop_env_of_formula gl form =
     Mc.(
       let rec doit env = function
-        | TT | FF | A (_, _) -> env
-        | X t -> fst (Env.compute_rank_add env t)
-        | Cj (f1, f2) | D (f1, f2) | I (f1, _, f2) -> doit (doit env f1) f2
-        | N f -> doit env f
+        | TT _ | FF _ | A (_, _, _) -> env
+        | X (b, t) -> fst (Env.compute_rank_add env t b)
+        | AND (b, f1, f2)
+         |OR (b, f1, f2)
+         |IMPL (b, f1, _, f2)
+         |IFF (b, f1, f2) ->
+          doit (doit env f1) f2
+        | NOT (b, f) -> doit env f
+        | EQ (f1, f2) -> doit (doit env f1) f2
       in
       doit (Env.empty gl) form)
 
@@ -1008,11 +1089,15 @@ module M = struct
     in
     Mc.(
       let rec doit = function
-        | TT | FF | X _ -> ISet.empty
-        | A (a, (t, c)) -> vars_of_atom a
-        | Cj (f1, f2) | D (f1, f2) | I (f1, _, f2) ->
+        | TT _ | FF _ | X _ -> ISet.empty
+        | A (_, a, (t, c)) -> vars_of_atom a
+        | AND (_, f1, f2)
+         |OR (_, f1, f2)
+         |IMPL (_, f1, _, f2)
+         |IFF (_, f1, f2)
+         |EQ (f1, f2) ->
           ISet.union (doit f1) (doit f2)
-        | N f -> doit f
+        | NOT (_, f) -> doit f
       in
       doit form)
 
@@ -1026,7 +1111,8 @@ module M = struct
     ; dump_mul : EConstr.constr
     ; dump_pow : EConstr.constr
     ; dump_pow_arg : Mc.n -> EConstr.constr
-    ; dump_op : (Mc.op2 * EConstr.constr) list }
+    ; dump_op_prop : (Mc.op2 * EConstr.constr) list
+    ; dump_op_bool : (Mc.op2 * EConstr.constr) list }
 
   let dump_zexpr =
     lazy
@@ -1038,7 +1124,9 @@ module M = struct
       ; dump_mul = Lazy.force coq_Zmult
       ; dump_pow = Lazy.force coq_Zpower
       ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n)))
-      ; dump_op = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table }
+      ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_prop
+      ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_bool
+      }
 
   let dump_qexpr =
     lazy
@@ -1050,7 +1138,9 @@ module M = struct
       ; dump_mul = Lazy.force coq_Qmult
       ; dump_pow = Lazy.force coq_Qpower
       ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n)))
-      ; dump_op = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table }
+      ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_prop
+      ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_bool
+      }
 
   let rec dump_Rcst_as_R cst =
     match cst with
@@ -1087,7 +1177,9 @@ module M = struct
       ; dump_mul = Lazy.force coq_Rmult
       ; dump_pow = Lazy.force coq_Rpower
       ; dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n)))
-      ; dump_op = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table }
+      ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_prop
+      ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_bool
+      }
 
   let prodn n env b =
     let rec prodrec = function
@@ -1105,6 +1197,10 @@ module M = struct
 
 *)
 
+  let eKind = function
+    | Mc.IsProp -> EConstr.mkProp
+    | Mc.IsBool -> Lazy.force coq_bool
+
   let make_goal_of_formula gl dexpr form =
     let vars_idx =
       List.mapi
@@ -1120,7 +1216,7 @@ module M = struct
     in
     let props_n =
       List.mapi
-        (fun i _ -> (fresh_prop "__p" (i + 1), EConstr.mkProp))
+        (fun i (_, k) -> (fresh_prop "__p" (i + 1), eKind k))
         (Env.elements props)
     in
     let var_name_pos =
@@ -1129,8 +1225,7 @@ module M = struct
     let dump_expr i e =
       let rec dump_expr = function
         | Mc.PEX n ->
-          EConstr.mkRel
-            (i + CList.assoc_f Int.equal (CoqToCaml.positive n) vars_idx)
+          EConstr.mkRel (i + List.assoc (CoqToCaml.positive n) vars_idx)
         | Mc.PEc z -> dexpr.dump_cst z
         | Mc.PEadd (e1, e2) ->
           EConstr.mkApp (dexpr.dump_add, [|dump_expr e1; dump_expr e2|])
@@ -1144,31 +1239,70 @@ module M = struct
       in
       dump_expr e
     in
-    let mkop op e1 e2 =
-      try
-        EConstr.mkApp
-          (CList.assoc_f Mutils.Hash.eq_op2 op dexpr.dump_op, [|e1; e2|])
+    let mkop_prop op e1 e2 =
+      try EConstr.mkApp (List.assoc op dexpr.dump_op_prop, [|e1; e2|])
+      with Not_found ->
+        EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|])
+    in
+    let dump_cstr_prop i {Mc.flhs; Mc.fop; Mc.frhs} =
+      mkop_prop fop (dump_expr i flhs) (dump_expr i frhs)
+    in
+    let mkop_bool op e1 e2 =
+      try EConstr.mkApp (List.assoc op dexpr.dump_op_bool, [|e1; e2|])
       with Not_found ->
-        EConstr.mkApp (Lazy.force coq_Eq, [|dexpr.interp_typ; e1; e2|])
+        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)
+    let dump_cstr_bool i {Mc.flhs; Mc.fop; Mc.frhs} =
+      mkop_bool fop (dump_expr i flhs) (dump_expr i frhs)
     in
-    let rec xdump pi xi f =
+    let rec xdump_prop pi xi f =
       match f with
-      | Mc.TT -> Lazy.force coq_True
-      | Mc.FF -> Lazy.force coq_False
-      | Mc.Cj (x, y) ->
-        EConstr.mkApp (Lazy.force coq_and, [|xdump pi xi x; xdump pi xi y|])
-      | Mc.D (x, y) ->
-        EConstr.mkApp (Lazy.force coq_or, [|xdump pi xi x; xdump pi xi y|])
-      | Mc.I (x, _, y) ->
-        EConstr.mkArrow (xdump pi xi x) Sorts.Relevant
-          (xdump (pi + 1) (xi + 1) y)
-      | Mc.N x ->
-        EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (Lazy.force coq_False)
-      | Mc.A (x, _) -> dump_cstr xi x
-      | Mc.X t ->
+      | Mc.TT _ -> Lazy.force coq_True
+      | Mc.FF _ -> Lazy.force coq_False
+      | Mc.AND (_, x, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_and, [|xdump_prop pi xi x; xdump_prop pi xi y|])
+      | Mc.OR (_, x, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_or, [|xdump_prop pi xi x; xdump_prop pi xi y|])
+      | Mc.IFF (_, x, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_iff, [|xdump_prop pi xi x; xdump_prop pi xi y|])
+      | Mc.IMPL (_, x, _, y) ->
+        EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant
+          (xdump_prop (pi + 1) (xi + 1) y)
+      | Mc.NOT (_, x) ->
+        EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant
+          (Lazy.force coq_False)
+      | Mc.EQ (x, y) ->
+        EConstr.mkApp
+          ( Lazy.force coq_eq
+          , [|Lazy.force coq_bool; xdump_bool pi xi x; xdump_bool pi xi y|] )
+      | Mc.A (_, x, _) -> dump_cstr_prop xi x
+      | Mc.X (_, t) ->
+        let idx = Env.get_rank props t in
+        EConstr.mkRel (pi + idx)
+    and xdump_bool pi xi f =
+      match f with
+      | Mc.TT _ -> Lazy.force coq_true
+      | Mc.FF _ -> Lazy.force coq_false
+      | Mc.AND (_, x, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_andb, [|xdump_bool pi xi x; xdump_bool pi xi y|])
+      | Mc.OR (_, x, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_orb, [|xdump_bool pi xi x; xdump_bool pi xi y|])
+      | Mc.IFF (_, x, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_eqb, [|xdump_bool pi xi x; xdump_bool pi xi y|])
+      | Mc.IMPL (_, x, _, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_implb, [|xdump_bool pi xi x; xdump_bool pi xi y|])
+      | Mc.NOT (_, x) ->
+        EConstr.mkApp (Lazy.force coq_negb, [|xdump_bool pi xi x|])
+      | Mc.EQ (x, y) -> assert false
+      | Mc.A (_, x, _) -> dump_cstr_bool xi x
+      | Mc.X (_, t) ->
         let idx = Env.get_rank props t in
         EConstr.mkRel (pi + idx)
     in
@@ -1179,12 +1313,12 @@ module M = struct
       let idx = Env.get_rank props p in
       EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx))
     in
-    let form' = Mc.mapX subst_prop form in
+    let form' = Mc.mapX (fun _ p -> subst_prop p) Mc.IsProp form in
     ( 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))
+           (xdump_prop (List.length vars_n) 0 form))
     , List.rev props_n
     , List.rev var_name_pos
     , form' )
@@ -1339,7 +1473,9 @@ let qq_domain_spec =
     ; coeff_eq = Mc.qeq_bool }
 
 let max_tag f =
-  1 + Tag.to_int (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) f (Tag.from 0))
+  1
+  + Tag.to_int
+      (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) Mc.IsProp f (Tag.from 0))
 
 (** Naive topological sort of constr according to the subterm-ordering *)
 
@@ -1364,7 +1500,9 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*)
             (set
                [ ( "__ff"
                  , ff
-                 , EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) )
+                 , EConstr.mkApp
+                     ( Lazy.force coq_Formula
+                     , [|formula_typ; Lazy.force coq_IsProp|] ) )
                ; ( "__varmap"
                  , vm
                  , EConstr.mkApp (Lazy.force coq_VarMap, [|spec.typ|]) )
@@ -1527,37 +1665,73 @@ let abstract_formula : TagSet.t -> 'a formula -> 'a formula =
  fun hyps f ->
   let to_constr =
     Mc.
-      { mkTT = Lazy.force coq_True
-      ; mkFF = Lazy.force coq_False
-      ; mkA = (fun a (tg, t) -> t)
-      ; mkCj =
+      { mkTT =
+          (let coq_True = Lazy.force coq_True in
+           let coq_true = Lazy.force coq_true in
+           function Mc.IsProp -> coq_True | Mc.IsBool -> coq_true)
+      ; mkFF =
+          (let coq_False = Lazy.force coq_False in
+           let coq_false = Lazy.force coq_false in
+           function Mc.IsProp -> coq_False | Mc.IsBool -> coq_false)
+      ; mkA = (fun k a (tg, t) -> t)
+      ; mkAND =
           (let coq_and = Lazy.force coq_and in
-           fun x y -> EConstr.mkApp (coq_and, [|x; y|]))
-      ; mkD =
+           let coq_andb = Lazy.force coq_andb in
+           fun k x y ->
+             EConstr.mkApp
+               ( (match k with Mc.IsProp -> coq_and | Mc.IsBool -> coq_andb)
+               , [|x; y|] ))
+      ; mkOR =
           (let coq_or = Lazy.force coq_or in
-           fun x y -> EConstr.mkApp (coq_or, [|x; y|]))
-      ; mkI = (fun x y -> EConstr.mkArrow x Sorts.Relevant y)
-      ; mkN =
+           let coq_orb = Lazy.force coq_orb in
+           fun k x y ->
+             EConstr.mkApp
+               ( (match k with Mc.IsProp -> coq_or | Mc.IsBool -> coq_orb)
+               , [|x; y|] ))
+      ; mkIMPL =
+          (fun k x y ->
+            match k with
+            | Mc.IsProp -> EConstr.mkArrow x Sorts.Relevant y
+            | Mc.IsBool -> EConstr.mkApp (Lazy.force coq_implb, [|x; y|]))
+      ; mkIFF =
+          (let coq_iff = Lazy.force coq_iff in
+           let coq_eqb = Lazy.force coq_eqb in
+           fun k x y ->
+             EConstr.mkApp
+               ( (match k with Mc.IsProp -> coq_iff | Mc.IsBool -> coq_eqb)
+               , [|x; y|] ))
+      ; mkNOT =
           (let coq_not = Lazy.force coq_not in
-           fun x -> EConstr.mkApp (coq_not, [|x|])) }
+           let coq_negb = Lazy.force coq_negb in
+           fun k x ->
+             EConstr.mkApp
+               ( (match k with Mc.IsProp -> coq_not | Mc.IsBool -> coq_negb)
+               , [|x|] ))
+      ; mkEQ =
+          (let coq_eq = Lazy.force coq_eq in
+           fun x y -> EConstr.mkApp (coq_eq, [|Lazy.force coq_bool; x; y|])) }
   in
-  Mc.abst_form to_constr (fun (t, _) -> TagSet.mem t hyps) true f
+  Mc.abst_form to_constr (fun (t, _) -> TagSet.mem t hyps) true Mc.IsProp f
 
 (* [abstract_wrt_formula] is used in contexts whre f1 is already an abstraction of f2   *)
 let rec abstract_wrt_formula f1 f2 =
   Mc.(
     match (f1, f2) with
-    | X c, _ -> X c
+    | X (b, c), _ -> X (b, c)
     | A _, A _ -> f2
-    | Cj (a, b), Cj (a', b') ->
-      Cj (abstract_wrt_formula a a', abstract_wrt_formula b b')
-    | D (a, b), D (a', b') ->
-      D (abstract_wrt_formula a a', abstract_wrt_formula b b')
-    | I (a, _, b), I (a', x, b') ->
-      I (abstract_wrt_formula a a', x, abstract_wrt_formula b b')
-    | FF, FF -> FF
-    | TT, TT -> TT
-    | N x, N y -> N (abstract_wrt_formula x y)
+    | AND (b, f1, f2), AND (_, f1', f2') ->
+      AND (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2')
+    | OR (b, f1, f2), OR (_, f1', f2') ->
+      OR (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2')
+    | IMPL (b, f1, _, f2), IMPL (_, f1', x, f2') ->
+      IMPL (b, abstract_wrt_formula f1 f1', x, abstract_wrt_formula f2 f2')
+    | IFF (b, f1, f2), IFF (_, f1', f2') ->
+      IFF (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2')
+    | EQ (f1, f2), EQ (f1', f2') ->
+      EQ (abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2')
+    | FF b, FF _ -> FF b
+    | TT b, TT _ -> TT b
+    | NOT (b, x), NOT (_, y) -> NOT (b, abstract_wrt_formula x y)
     | _ -> failwith "abstract_wrt_formula")
 
 (**
@@ -1577,7 +1751,7 @@ let formula_hyps_concl hyps concl =
     (fun (id, f) (cc, ids) ->
       match f with
       | Mc.X _ -> (cc, ids)
-      | _ -> (Mc.I (f, Some id, cc), id :: ids))
+      | _ -> (Mc.IMPL (Mc.IsProp, f, Some id, cc), id :: ids))
     hyps (concl, [])
 
 (* let time str f x =
@@ -1595,7 +1769,7 @@ let micromega_tauto pre_process cnf spec prover env
   let mt = CamlToCoq.positive (max_tag ff) in
   (* Construction of cnf *)
   let pre_ff = pre_process mt (ff : 'a formula) in
-  let cnf_ff, cnf_ff_tags = cnf pre_ff in
+  let cnf_ff, cnf_ff_tags = cnf Mc.IsProp pre_ff in
   match witness_list_tags prover cnf_ff with
   | Model m -> Model m
   | Unknown -> Unknown
@@ -1621,7 +1795,7 @@ let micromega_tauto pre_process cnf spec prover env
     in
     let ff' = abstract_formula deps ff in
     let pre_ff' = pre_process mt ff' in
-    let cnf_ff', _ = cnf pre_ff' in
+    let cnf_ff', _ = cnf Mc.IsProp pre_ff' in
     if debug then begin
       output_string stdout "\n";
       Printf.printf "TForm    : %a\n" pp_formula ff;
@@ -1647,7 +1821,7 @@ let micromega_tauto pre_process cnf spec prover env
            | Some res -> ()
        end ; *)
     let res' = compact_proofs spec.coeff_eq cnf_ff res cnf_ff' in
-    let ff', res', ids = (ff', res', Mc.ids_of_formula ff') in
+    let ff', res', ids = (ff', res', Mc.ids_of_formula Mc.IsProp ff') in
     let res' = dump_list spec.proof_typ spec.dump_proof res' in
     Prf (ids, ff', res')
 
@@ -1719,9 +1893,11 @@ let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac =
                   env' ff_arith ]
           in
           let goal_props =
-            List.rev (Env.elements (prop_env_of_formula gl0 ff'))
+            List.rev (List.map fst (Env.elements (prop_env_of_formula gl0 ff')))
+          in
+          let goal_vars =
+            List.map (fun (_, i) -> fst (List.nth env (i - 1))) vars
           in
-          let goal_vars = List.map (fun (_, i) -> List.nth env (i - 1)) vars in
           let arith_args = goal_props @ goal_vars in
           let kill_arith = Tacticals.New.tclTHEN tac_arith tac in
           (*
@@ -1773,7 +1949,9 @@ let micromega_order_changer cert env ff =
             (set
                [ ( "__ff"
                  , ff
-                 , EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) )
+                 , EConstr.mkApp
+                     ( Lazy.force coq_Formula
+                     , [|formula_typ; Lazy.force coq_IsProp|] ) )
                ; ("__varmap", vm, EConstr.mkApp (Lazy.force coq_VarMap, [|typ|]))
                ; ("__wit", cert, cert_typ) ]
                (Tacmach.New.pf_concl gl))
@@ -1805,11 +1983,16 @@ let micromega_genr prover tac =
         let hyps' =
           List.map
             (fun (n, f) ->
-              (n, Mc.map_bformula (Micromega.map_Formula Micromega.q_of_Rcst) f))
+              ( n
+              , Mc.map_bformula Mc.IsProp
+                  (Micromega.map_Formula Micromega.q_of_Rcst)
+                  f ))
             hyps
         in
         let concl' =
-          Mc.map_bformula (Micromega.map_Formula Micromega.q_of_Rcst) concl
+          Mc.map_bformula Mc.IsProp
+            (Micromega.map_Formula Micromega.q_of_Rcst)
+            concl
         in
         match
           micromega_tauto
@@ -1847,9 +2030,11 @@ let micromega_genr prover tac =
               ; micromega_order_changer res' env' ff_arith ]
           in
           let goal_props =
-            List.rev (Env.elements (prop_env_of_formula gl0 ff'))
+            List.rev (List.map fst (Env.elements (prop_env_of_formula gl0 ff')))
+          in
+          let goal_vars =
+            List.map (fun (_, i) -> fst (List.nth env (i - 1))) vars
           in
-          let goal_vars = List.map (fun (_, i) -> List.nth env (i - 1)) vars in
           let arith_args = goal_props @ goal_vars in
           let kill_arith = Tacticals.New.tclTHEN tac_arith tac in
           (* Tacticals.New.tclTHEN
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index d17a0aabb7..b231779c7b 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -967,39 +967,49 @@ let rec norm_aux cO cI cadd cmul csub copp ceqb = function
   ppow_N cO cI cadd cmul ceqb (fun p -> p)
     (norm_aux cO cI cadd cmul csub copp ceqb pe1) n0
 
+type kind =
+| IsProp
+| IsBool
+
 type ('tA, 'tX, 'aA, 'aF) gFormula =
-| TT
-| FF
-| X of 'tX
-| A of 'tA * 'aA
-| Cj of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
-| D of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
-| N of ('tA, 'tX, 'aA, 'aF) gFormula
-| I of ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option
+| TT of kind
+| FF of kind
+| X of kind * 'tX
+| A of kind * 'tA * 'aA
+| AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+| OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+| NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula
+| IMPL of kind * ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option
    * ('tA, 'tX, 'aA, 'aF) gFormula
+| IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+| EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
 
 (** val mapX :
-    ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4)
-    gFormula **)
-
-let rec mapX f = function
-| X x -> X (f x)
-| Cj (f1, f2) -> Cj ((mapX f f1), (mapX f f2))
-| D (f1, f2) -> D ((mapX f f1), (mapX f f2))
-| N f1 -> N (mapX f f1)
-| I (f1, o, f2) -> I ((mapX f f1), o, (mapX f f2))
+    (kind -> 'a2 -> 'a2) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1,
+    'a2, 'a3, 'a4) gFormula **)
+
+let rec mapX f _ = function
+| X (k0, x) -> X (k0, (f k0 x))
+| AND (k0, f1, f2) -> AND (k0, (mapX f k0 f1), (mapX f k0 f2))
+| OR (k0, f1, f2) -> OR (k0, (mapX f k0 f1), (mapX f k0 f2))
+| NOT (k0, f1) -> NOT (k0, (mapX f k0 f1))
+| IMPL (k0, f1, o, f2) -> IMPL (k0, (mapX f k0 f1), o, (mapX f k0 f2))
+| IFF (k0, f1, f2) -> IFF (k0, (mapX f k0 f1), (mapX f k0 f2))
+| EQ (f1, f2) -> EQ ((mapX f IsBool f1), (mapX f IsBool f2))
 | x -> x
 
 (** val foldA :
-    ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 **)
+    ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 **)
 
-let rec foldA f f0 acc =
+let rec foldA f _ f0 acc =
   match f0 with
-  | A (_, an) -> f acc an
-  | Cj (f1, f2) -> foldA f f1 (foldA f f2 acc)
-  | D (f1, f2) -> foldA f f1 (foldA f f2 acc)
-  | N f1 -> foldA f f1 acc
-  | I (f1, _, f2) -> foldA f f1 (foldA f f2 acc)
+  | A (_, _, an) -> f acc an
+  | AND (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc)
+  | OR (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc)
+  | NOT (k0, f1) -> foldA f k0 f1 acc
+  | IMPL (k0, f1, _, f2) -> foldA f k0 f1 (foldA f k0 f2 acc)
+  | IFF (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc)
+  | EQ (f1, f2) -> foldA f IsBool f1 (foldA f IsBool f2 acc)
   | _ -> acc
 
 (** val cons_id : 'a1 option -> 'a1 list -> 'a1 list **)
@@ -1009,37 +1019,50 @@ let cons_id id l =
   | Some id0 -> id0::l
   | None -> l
 
-(** val ids_of_formula : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list **)
+(** val ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list **)
 
-let rec ids_of_formula = function
-| I (_, id, f') -> cons_id id (ids_of_formula f')
+let rec ids_of_formula _ = function
+| IMPL (k0, _, id, f') -> cons_id id (ids_of_formula k0 f')
 | _ -> []
 
-(** val collect_annot : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list **)
+(** val collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list **)
 
-let rec collect_annot = function
-| A (_, a) -> a::[]
-| Cj (f1, f2) -> app (collect_annot f1) (collect_annot f2)
-| D (f1, f2) -> app (collect_annot f1) (collect_annot f2)
-| N f0 -> collect_annot f0
-| I (f1, _, f2) -> app (collect_annot f1) (collect_annot f2)
+let rec collect_annot _ = function
+| A (_, _, a) -> a::[]
+| AND (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2)
+| OR (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2)
+| NOT (k0, f0) -> collect_annot k0 f0
+| IMPL (k0, f1, _, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2)
+| IFF (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2)
+| EQ (f1, f2) -> app (collect_annot IsBool f1) (collect_annot IsBool f2)
 | _ -> []
 
-type 'a bFormula = ('a, __, unit0, unit0) gFormula
+type rtyp = __
+
+type eKind = __
+
+type 'a bFormula = ('a, eKind, unit0, unit0) gFormula
 
 (** val map_bformula :
-    ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5)
-    gFormula **)
-
-let rec map_bformula fct = function
-| TT -> TT
-| FF -> FF
-| X p -> X p
-| A (a, t0) -> A ((fct a), t0)
-| 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, a, f2) -> I ((map_bformula fct f1), a, (map_bformula fct f2))
+    kind -> ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4,
+    'a5) gFormula **)
+
+let rec map_bformula _ fct = function
+| TT k -> TT k
+| FF k -> FF k
+| X (k, p) -> X (k, p)
+| A (k, a, t0) -> A (k, (fct a), t0)
+| AND (k0, f1, f2) ->
+  AND (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2))
+| OR (k0, f1, f2) ->
+  OR (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2))
+| NOT (k0, f0) -> NOT (k0, (map_bformula k0 fct f0))
+| IMPL (k0, f1, a, f2) ->
+  IMPL (k0, (map_bformula k0 fct f1), a, (map_bformula k0 fct f2))
+| IFF (k0, f1, f2) ->
+  IFF (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2))
+| EQ (f1, f2) ->
+  EQ ((map_bformula IsBool fct f1), (map_bformula IsBool fct f2))
 
 type ('x, 'annot) clause = ('x * 'annot) list
 
@@ -1147,7 +1170,7 @@ let is_cnf_ff = function
 let and_cnf_opt f1 f2 =
   if if is_cnf_ff f1 then true else is_cnf_ff f2
   then cnf_ff
-  else and_cnf f1 f2
+  else if is_cnf_tt f2 then f1 else and_cnf f1 f2
 
 (** val or_cnf_opt :
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1,
@@ -1158,36 +1181,89 @@ let or_cnf_opt unsat deduce f1 f2 =
   then cnf_tt
   else if is_cnf_ff f2 then f1 else or_cnf unsat deduce f1 f2
 
-(** val xcnf :
-    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3)
-    cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5)
-    tFormula -> ('a2, 'a3) cnf **)
-
-let rec xcnf unsat deduce normalise1 negate0 pol0 = function
-| TT -> if pol0 then cnf_tt else cnf_ff
-| FF -> if pol0 then cnf_ff else cnf_tt
-| X _ -> cnf_ff
-| A (x, t0) -> if pol0 then normalise1 x t0 else negate0 x t0
-| Cj (e1, e2) ->
+(** val mk_and :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3,
+    'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **)
+
+let mk_and unsat deduce rEC k pol0 f1 f2 =
   if pol0
-  then and_cnf_opt (xcnf unsat deduce normalise1 negate0 pol0 e1)
-         (xcnf unsat deduce normalise1 negate0 pol0 e2)
-  else or_cnf_opt unsat deduce (xcnf unsat deduce normalise1 negate0 pol0 e1)
-         (xcnf unsat deduce normalise1 negate0 pol0 e2)
-| D (e1, e2) ->
+  then and_cnf_opt (rEC pol0 k f1) (rEC pol0 k f2)
+  else or_cnf_opt unsat deduce (rEC pol0 k f1) (rEC pol0 k f2)
+
+(** val mk_or :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3,
+    'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **)
+
+let mk_or unsat deduce rEC k pol0 f1 f2 =
   if pol0
-  then or_cnf_opt unsat deduce (xcnf unsat deduce normalise1 negate0 pol0 e1)
-         (xcnf unsat deduce normalise1 negate0 pol0 e2)
-  else and_cnf_opt (xcnf unsat deduce normalise1 negate0 pol0 e1)
-         (xcnf unsat deduce normalise1 negate0 pol0 e2)
-| N e -> xcnf unsat deduce normalise1 negate0 (negb pol0) e
-| I (e1, _, e2) ->
+  then or_cnf_opt unsat deduce (rEC pol0 k f1) (rEC pol0 k f2)
+  else and_cnf_opt (rEC pol0 k f1) (rEC pol0 k f2)
+
+(** val mk_impl :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3,
+    'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **)
+
+let mk_impl unsat deduce rEC k pol0 f1 f2 =
   if pol0
-  then or_cnf_opt unsat deduce
-         (xcnf unsat deduce normalise1 negate0 (negb pol0) e1)
-         (xcnf unsat deduce normalise1 negate0 pol0 e2)
-  else and_cnf_opt (xcnf unsat deduce normalise1 negate0 (negb pol0) e1)
-         (xcnf unsat deduce normalise1 negate0 pol0 e2)
+  then or_cnf_opt unsat deduce (rEC (negb pol0) k f1) (rEC pol0 k f2)
+  else and_cnf_opt (rEC (negb pol0) k f1) (rEC pol0 k f2)
+
+(** val mk_iff :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3,
+    'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **)
+
+let mk_iff unsat deduce rEC k pol0 f1 f2 =
+  or_cnf_opt unsat deduce
+    (and_cnf_opt (rEC (negb pol0) k f1) (rEC false k f2))
+    (and_cnf_opt (rEC pol0 k f1) (rEC true k f2))
+
+(** val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option **)
+
+let is_bool _ = function
+| TT _ -> Some true
+| FF _ -> Some false
+| _ -> None
+
+(** val xcnf :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3)
+    cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4,
+    'a5) tFormula -> ('a2, 'a3) cnf **)
+
+let rec xcnf unsat deduce normalise1 negate0 pol0 _ = function
+| TT _ -> if pol0 then cnf_tt else cnf_ff
+| FF _ -> if pol0 then cnf_ff else cnf_tt
+| X (_, _) -> cnf_ff
+| A (_, x, t0) -> if pol0 then normalise1 x t0 else negate0 x t0
+| AND (k0, e1, e2) ->
+  mk_and unsat deduce (fun x x0 x1 ->
+    xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2
+| OR (k0, e1, e2) ->
+  mk_or unsat deduce (fun x x0 x1 ->
+    xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2
+| NOT (k0, e) -> xcnf unsat deduce normalise1 negate0 (negb pol0) k0 e
+| IMPL (k0, e1, _, e2) ->
+  mk_impl unsat deduce (fun x x0 x1 ->
+    xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2
+| IFF (k0, e1, e2) ->
+  (match is_bool k0 e2 with
+   | Some isb ->
+     xcnf unsat deduce normalise1 negate0 (if isb then pol0 else negb pol0)
+       k0 e1
+   | None ->
+     mk_iff unsat deduce (fun x x0 x1 ->
+       xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2)
+| EQ (e1, e2) ->
+  (match is_bool IsBool e2 with
+   | Some isb ->
+     xcnf unsat deduce normalise1 negate0 (if isb then pol0 else negb pol0)
+       IsBool e1
+   | None ->
+     mk_iff unsat deduce (fun x x0 x1 ->
+       xcnf unsat deduce normalise1 negate0 x x0 x1) IsBool pol0 e1 e2)
 
 (** val radd_term :
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2)
@@ -1271,141 +1347,311 @@ let ror_cnf_opt unsat deduce f1 f2 =
 let ratom c a =
   if if is_cnf_ff c then true else is_cnf_tt c then c,(a::[]) else c,[]
 
-(** val rxcnf :
-    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3)
-    cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5)
-    tFormula -> ('a2, 'a3) cnf * 'a3 list **)
-
-let rec rxcnf unsat deduce normalise1 negate0 polarity = function
-| TT -> if polarity then cnf_tt,[] else cnf_ff,[]
-| FF -> if polarity then cnf_ff,[] else cnf_tt,[]
-| X _ -> cnf_ff,[]
-| A (x, t0) -> ratom (if polarity then normalise1 x t0 else negate0 x t0) t0
-| Cj (e1, e2) ->
-  let e3,t1 = rxcnf unsat deduce normalise1 negate0 polarity e1 in
-  let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in
+(** val rxcnf_and :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind ->
+    ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2,
+    'a3) cnf * 'a3 list **)
+
+let rxcnf_and unsat deduce rXCNF polarity k e1 e2 =
+  let e3,t1 = rXCNF polarity k e1 in
+  let e4,t2 = rXCNF polarity k e2 in
   if polarity
   then (and_cnf_opt e3 e4),(rev_append t1 t2)
   else let f',t' = ror_cnf_opt unsat deduce e3 e4 in
        f',(rev_append t1 (rev_append t2 t'))
-| D (e1, e2) ->
-  let e3,t1 = rxcnf unsat deduce normalise1 negate0 polarity e1 in
-  let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in
+
+(** val rxcnf_or :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind ->
+    ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2,
+    'a3) cnf * 'a3 list **)
+
+let rxcnf_or unsat deduce rXCNF polarity k e1 e2 =
+  let e3,t1 = rXCNF polarity k e1 in
+  let e4,t2 = rXCNF polarity k e2 in
   if polarity
   then let f',t' = ror_cnf_opt unsat deduce e3 e4 in
        f',(rev_append t1 (rev_append t2 t'))
   else (and_cnf_opt e3 e4),(rev_append t1 t2)
-| N e -> rxcnf unsat deduce normalise1 negate0 (negb polarity) e
-| I (e1, _, e2) ->
-  let e3,t1 = rxcnf unsat deduce normalise1 negate0 (negb polarity) e1 in
+
+(** val rxcnf_impl :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind ->
+    ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2,
+    'a3) cnf * 'a3 list **)
+
+let rxcnf_impl unsat deduce rXCNF polarity k e1 e2 =
+  let e3,t1 = rXCNF (negb polarity) k e1 in
   if polarity
   then if is_cnf_ff e3
-       then rxcnf unsat deduce normalise1 negate0 polarity e2
-       else let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in
+       then rXCNF polarity k e2
+       else let e4,t2 = rXCNF polarity k e2 in
             let f',t' = ror_cnf_opt unsat deduce e3 e4 in
             f',(rev_append t1 (rev_append t2 t'))
-  else let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in
+  else let e4,t2 = rXCNF polarity k e2 in
        (and_cnf_opt e3 e4),(rev_append t1 t2)
 
-type ('term, 'annot, 'tX) to_constrT = { mkTT : 'tX; mkFF : 'tX;
-                                         mkA : ('term -> 'annot -> 'tX);
-                                         mkCj : ('tX -> 'tX -> 'tX);
-                                         mkD : ('tX -> 'tX -> 'tX);
-                                         mkI : ('tX -> 'tX -> 'tX);
-                                         mkN : ('tX -> 'tX) }
+(** val rxcnf_iff :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind ->
+    ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2,
+    'a3) cnf * 'a3 list **)
+
+let rxcnf_iff unsat deduce rXCNF polarity k e1 e2 =
+  let c1,t1 = rXCNF (negb polarity) k e1 in
+  let c2,t2 = rXCNF false k e2 in
+  let c3,t3 = rXCNF polarity k e1 in
+  let c4,t4 = rXCNF true k e2 in
+  let f',t' = ror_cnf_opt unsat deduce (and_cnf_opt c1 c2) (and_cnf_opt c3 c4)
+  in
+  f',(rev_append t1 (rev_append t2 (rev_append t3 (rev_append t4 t'))))
+
+(** val rxcnf :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3)
+    cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4,
+    'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list **)
+
+let rec rxcnf unsat deduce normalise1 negate0 polarity _ = function
+| TT _ -> if polarity then cnf_tt,[] else cnf_ff,[]
+| FF _ -> if polarity then cnf_ff,[] else cnf_tt,[]
+| X (_, _) -> cnf_ff,[]
+| A (_, x, t0) ->
+  ratom (if polarity then normalise1 x t0 else negate0 x t0) t0
+| AND (k0, e1, e2) ->
+  rxcnf_and unsat deduce (fun x x0 x1 ->
+    rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2
+| OR (k0, e1, e2) ->
+  rxcnf_or unsat deduce (fun x x0 x1 ->
+    rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2
+| NOT (k0, e) -> rxcnf unsat deduce normalise1 negate0 (negb polarity) k0 e
+| IMPL (k0, e1, _, e2) ->
+  rxcnf_impl unsat deduce (fun x x0 x1 ->
+    rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2
+| IFF (k0, e1, e2) ->
+  rxcnf_iff unsat deduce (fun x x0 x1 ->
+    rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2
+| EQ (e1, e2) ->
+  rxcnf_iff unsat deduce (fun x x0 x1 ->
+    rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity IsBool e1 e2
+
+type ('term, 'annot, 'tX) to_constrT = { mkTT : (kind -> 'tX);
+                                         mkFF : (kind -> 'tX);
+                                         mkA : (kind -> 'term -> 'annot ->
+                                               'tX);
+                                         mkAND : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkOR : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkIMPL : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkIFF : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkNOT : (kind -> 'tX -> 'tX);
+                                         mkEQ : ('tX -> 'tX -> 'tX) }
 
 (** val aformula :
-    ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 **)
-
-let rec aformula to_constr = function
-| TT -> to_constr.mkTT
-| FF -> to_constr.mkFF
-| X p -> p
-| A (x, t0) -> to_constr.mkA x t0
-| Cj (f1, f2) ->
-  to_constr.mkCj (aformula to_constr f1) (aformula to_constr f2)
-| D (f1, f2) -> to_constr.mkD (aformula to_constr f1) (aformula to_constr f2)
-| N f0 -> to_constr.mkN (aformula to_constr f0)
-| I (f1, _, f2) ->
-  to_constr.mkI (aformula to_constr f1) (aformula to_constr f2)
-
-(** val is_X : ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option **)
-
-let is_X = function
-| X p -> Some p
+    ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 **)
+
+let rec aformula to_constr _ = function
+| TT b -> to_constr.mkTT b
+| FF b -> to_constr.mkFF b
+| X (_, p) -> p
+| A (b, x, t0) -> to_constr.mkA b x t0
+| AND (k0, f1, f2) ->
+  to_constr.mkAND k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2)
+| OR (k0, f1, f2) ->
+  to_constr.mkOR k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2)
+| NOT (k0, f0) -> to_constr.mkNOT k0 (aformula to_constr k0 f0)
+| IMPL (k0, f1, _, f2) ->
+  to_constr.mkIMPL k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2)
+| IFF (k0, f1, f2) ->
+  to_constr.mkIFF k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2)
+| EQ (f1, f2) ->
+  to_constr.mkEQ (aformula to_constr IsBool f1) (aformula to_constr IsBool f2)
+
+(** val is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option **)
+
+let is_X _ = function
+| X (_, p) -> Some p
 | _ -> None
 
 (** val abs_and :
-    ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2,
-    'a3, 'a4) tFormula -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
-    'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4)
-    gFormula **)
-
-let abs_and to_constr f1 f2 c =
-  match is_X f1 with
-  | Some _ -> X (aformula to_constr (c f1 f2))
+    ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula
+    -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) ->
+    ('a1, 'a3, 'a2, 'a4) gFormula **)
+
+let abs_and to_constr k f1 f2 c =
+  match is_X k f1 with
+  | Some _ -> X (k, (aformula to_constr k (c k f1 f2)))
   | None ->
-    (match is_X f2 with
-     | Some _ -> X (aformula to_constr (c f1 f2))
-     | None -> c f1 f2)
+    (match is_X k f2 with
+     | Some _ -> X (k, (aformula to_constr k (c k f1 f2)))
+     | None -> c k f1 f2)
 
 (** val abs_or :
-    ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2,
-    'a3, 'a4) tFormula -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
-    'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4)
-    gFormula **)
+    ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula
+    -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) ->
+    ('a1, 'a3, 'a2, 'a4) gFormula **)
 
-let abs_or to_constr f1 f2 c =
-  match is_X f1 with
+let abs_or to_constr k f1 f2 c =
+  match is_X k f1 with
   | Some _ ->
-    (match is_X f2 with
-     | Some _ -> X (aformula to_constr (c f1 f2))
-     | None -> c f1 f2)
-  | None -> c f1 f2
+    (match is_X k f2 with
+     | Some _ -> X (k, (aformula to_constr k (c k f1 f2)))
+     | None -> c k f1 f2)
+  | None -> c k f1 f2
+
+(** val abs_not :
+    ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula)
+    -> ('a1, 'a3, 'a2, 'a4) gFormula **)
+
+let abs_not to_constr k f1 c =
+  match is_X k f1 with
+  | Some _ -> X (k, (aformula to_constr k (c k f1)))
+  | None -> c k f1
 
 (** val mk_arrow :
-    'a4 option -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4)
-    tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **)
+    'a4 option -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
+    'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **)
 
-let mk_arrow o f1 f2 =
+let mk_arrow o k f1 f2 =
   match o with
-  | Some _ -> (match is_X f1 with
-               | Some _ -> f2
-               | None -> I (f1, o, f2))
-  | None -> I (f1, None, f2)
+  | Some _ ->
+    (match is_X k f1 with
+     | Some _ -> f2
+     | None -> IMPL (k, f1, o, f2))
+  | None -> IMPL (k, f1, None, f2)
+
+(** val abst_simpl :
+    ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> kind -> ('a1, 'a2, 'a3,
+    'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **)
+
+let rec abst_simpl to_constr needA _ = function
+| A (k, x, t0) ->
+  if needA t0 then A (k, x, t0) else X (k, (to_constr.mkA k x t0))
+| AND (k0, f1, f2) ->
+  AND (k0, (abst_simpl to_constr needA k0 f1),
+    (abst_simpl to_constr needA k0 f2))
+| OR (k0, f1, f2) ->
+  OR (k0, (abst_simpl to_constr needA k0 f1),
+    (abst_simpl to_constr needA k0 f2))
+| NOT (k0, f0) -> NOT (k0, (abst_simpl to_constr needA k0 f0))
+| IMPL (k0, f1, o, f2) ->
+  IMPL (k0, (abst_simpl to_constr needA k0 f1), o,
+    (abst_simpl to_constr needA k0 f2))
+| IFF (k0, f1, f2) ->
+  IFF (k0, (abst_simpl to_constr needA k0 f1),
+    (abst_simpl to_constr needA k0 f2))
+| EQ (f1, f2) ->
+  EQ ((abst_simpl to_constr needA IsBool f1),
+    (abst_simpl to_constr needA IsBool f2))
+| x -> x
 
-(** val abst_form :
-    ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> ('a1, 'a2, 'a3,
-    'a4) tFormula -> ('a1, 'a3, 'a2, 'a4) gFormula **)
-
-let rec abst_form to_constr needA pol0 = function
-| TT -> if pol0 then TT else X to_constr.mkTT
-| FF -> if pol0 then X to_constr.mkFF else FF
-| X p -> X p
-| A (x, t0) -> if needA t0 then A (x, t0) else X (to_constr.mkA x t0)
-| Cj (f1, f2) ->
-  let f3 = abst_form to_constr needA pol0 f1 in
-  let f4 = abst_form to_constr needA pol0 f2 in
+(** val abst_and :
+    ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4)
+    tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2,
+    'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
+    'a4) tFormula **)
+
+let abst_and to_constr rEC pol0 k f1 f2 =
   if pol0
-  then abs_and to_constr f3 f4 (fun x x0 -> Cj (x, x0))
-  else abs_or to_constr f3 f4 (fun x x0 -> Cj (x, x0))
-| D (f1, f2) ->
-  let f3 = abst_form to_constr needA pol0 f1 in
-  let f4 = abst_form to_constr needA pol0 f2 in
+  then abs_and to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 ->
+         AND (x, x0, x1))
+  else abs_or to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> AND
+         (x, x0, x1))
+
+(** val abst_or :
+    ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4)
+    tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2,
+    'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
+    'a4) tFormula **)
+
+let abst_or to_constr rEC pol0 k f1 f2 =
   if pol0
-  then abs_or to_constr f3 f4 (fun x x0 -> D (x, x0))
-  else abs_and to_constr f3 f4 (fun x x0 -> D (x, x0))
-| N f0 ->
-  let f1 = abst_form to_constr needA (negb pol0) f0 in
-  (match is_X f1 with
-   | Some a -> X (to_constr.mkN a)
-   | None -> N f1)
-| I (f1, o, f2) ->
-  let f3 = abst_form to_constr needA (negb pol0) f1 in
-  let f4 = abst_form to_constr needA pol0 f2 in
+  then abs_or to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> OR
+         (x, x0, x1))
+  else abs_and to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> OR
+         (x, x0, x1))
+
+(** val abst_impl :
+    ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4)
+    tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> 'a4 option -> kind
+    -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    ('a1, 'a2, 'a3, 'a4) tFormula **)
+
+let abst_impl to_constr rEC pol0 o k f1 f2 =
   if pol0
-  then abs_or to_constr f3 f4 (mk_arrow o)
-  else abs_and to_constr f3 f4 (mk_arrow o)
+  then abs_or to_constr k (rEC (negb pol0) k f1) (rEC pol0 k f2) (mk_arrow o)
+  else abs_and to_constr k (rEC (negb pol0) k f1) (rEC pol0 k f2) (mk_arrow o)
+
+(** val or_is_X :
+    kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    bool **)
+
+let or_is_X k f1 f2 =
+  match is_X k f1 with
+  | Some _ -> true
+  | None -> (match is_X k f2 with
+             | Some _ -> true
+             | None -> false)
+
+(** val abs_iff :
+    ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1,
+    'a2, 'a3, 'a4) tFormula -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1,
+    'a2, 'a3, 'a4) tFormula **)
+
+let abs_iff to_constr k nf1 ff2 f1 tf2 r def =
+  if (&&) (or_is_X k nf1 ff2) (or_is_X k f1 tf2)
+  then X (r, (aformula to_constr r def))
+  else def
+
+(** val abst_iff :
+    ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1,
+    'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind
+    -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    ('a1, 'a2, 'a3, 'a4) tFormula **)
+
+let abst_iff to_constr needA rEC pol0 k f1 f2 =
+  abs_iff to_constr k (rEC (negb pol0) k f1) (rEC false k f2) (rEC pol0 k f1)
+    (rEC true k f2) k (IFF (k, (abst_simpl to_constr needA k f1),
+    (abst_simpl to_constr needA k f2)))
+
+(** val abst_eq :
+    ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1,
+    'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool ->
+    ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1,
+    'a2, 'a3, 'a4) tFormula **)
+
+let abst_eq to_constr needA rEC pol0 f1 f2 =
+  abs_iff to_constr IsBool (rEC (negb pol0) IsBool f1) (rEC false IsBool f2)
+    (rEC pol0 IsBool f1) (rEC true IsBool f2) IsProp (EQ
+    ((abst_simpl to_constr needA IsBool f1),
+    (abst_simpl to_constr needA IsBool f2)))
+
+(** val abst_form :
+    ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> kind -> ('a1, 'a2,
+    'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **)
+
+let rec abst_form to_constr needA pol0 _ = function
+| TT k -> if pol0 then TT k else X (k, (to_constr.mkTT k))
+| FF k -> if pol0 then X (k, (to_constr.mkFF k)) else FF k
+| X (k, p) -> X (k, p)
+| A (k, x, t0) ->
+  if needA t0 then A (k, x, t0) else X (k, (to_constr.mkA k x t0))
+| AND (k0, f1, f2) ->
+  abst_and to_constr (abst_form to_constr needA) pol0 k0 f1 f2
+| OR (k0, f1, f2) ->
+  abst_or to_constr (abst_form to_constr needA) pol0 k0 f1 f2
+| NOT (k0, f0) ->
+  abs_not to_constr k0 (abst_form to_constr needA (negb pol0) k0 f0)
+    (fun x x0 -> NOT (x, x0))
+| IMPL (k0, f1, o, f2) ->
+  abst_impl to_constr (abst_form to_constr needA) pol0 o k0 f1 f2
+| IFF (k0, f1, f2) ->
+  abst_iff to_constr needA (abst_form to_constr needA) pol0 k0 f1 f2
+| EQ (f1, f2) ->
+  abst_eq to_constr needA (abst_form to_constr needA) pol0 f1 f2
 
 (** val cnf_checker :
     (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool **)
@@ -1421,10 +1667,10 @@ let rec cnf_checker checker f l =
 (** val tauto_checker :
     ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3)
     cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 ->
-    bool) -> ('a1, __, 'a3, unit0) gFormula -> 'a4 list -> bool **)
+    bool) -> ('a1, rtyp, 'a3, unit0) gFormula -> 'a4 list -> bool **)
 
 let tauto_checker unsat deduce normalise1 negate0 checker f w =
-  cnf_checker checker (xcnf unsat deduce normalise1 negate0 true f) w
+  cnf_checker checker (xcnf unsat deduce normalise1 negate0 true IsProp f) w
 
 (** val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool **)
 
@@ -1969,10 +2215,11 @@ let negate t0 tg =
   if zunsat f then cnf_tt else cnf_of_list0 tg (xnegate0 f)
 
 (** val cnfZ :
-    (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list **)
+    kind -> (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1)
+    cnf * 'a1 list **)
 
-let cnfZ f =
-  rxcnf zunsat zdeduce normalise0 negate true f
+let cnfZ k f =
+  rxcnf zunsat zdeduce normalise0 negate true k f
 
 (** val ceiling : z -> z -> z **)
 
@@ -2178,10 +2425,11 @@ let normQ =
     qminus qopp qeq_bool
 
 (** val cnfQ :
-    (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 list **)
+    kind -> (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1)
+    cnf * 'a1 list **)
 
-let cnfQ f =
-  rxcnf qunsat qdeduce qnormalise qnegate true f
+let cnfQ k f =
+  rxcnf qunsat qdeduce qnormalise qnegate true k f
 
 (** val qTautoChecker : q formula bFormula -> qWitness list -> bool **)
 
@@ -2255,4 +2503,5 @@ let rdeduce =
 
 let rTautoChecker f w =
   tauto_checker runsat rdeduce rnormalise rnegate (fun cl ->
-    rWeakChecker (map fst cl)) (map_bformula (map_Formula q_of_Rcst) f) w
+    rWeakChecker (map fst cl))
+    (map_bformula IsProp (map_Formula q_of_Rcst) f) w
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 4200c80574..53f62e0f5b 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -88,6 +88,15 @@ end
 
 val zeq_bool : z -> z -> bool
 
+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
+
 type 'c pol =
   | Pc of 'c
   | Pinj of positive * 'c pol
@@ -209,15 +218,6 @@ val psquare :
   -> '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 :
@@ -254,29 +254,46 @@ val norm_aux :
   -> 'a1 pExpr
   -> 'a1 pol
 
+type kind = IsProp | IsBool
+
 type ('tA, 'tX, 'aA, 'aF) gFormula =
-  | TT
-  | FF
-  | X of 'tX
-  | A of 'tA * 'aA
-  | Cj of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
-  | D of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
-  | N of ('tA, 'tX, 'aA, 'aF) gFormula
-  | I of
-      ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula
+  | TT of kind
+  | FF of kind
+  | X of kind * 'tX
+  | A of kind * 'tA * 'aA
+  | AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+  | OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+  | NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula
+  | IMPL of
+      kind
+      * ('tA, 'tX, 'aA, 'aF) gFormula
+      * 'aF option
+      * ('tA, 'tX, 'aA, 'aF) gFormula
+  | IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+  | EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
 
 val mapX :
-  ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula
+     (kind -> 'a2 -> 'a2)
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) gFormula
+  -> ('a1, 'a2, 'a3, 'a4) gFormula
+
+val foldA :
+  ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5
 
-val foldA : ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5
 val cons_id : 'a1 option -> 'a1 list -> 'a1 list
-val ids_of_formula : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list
-val collect_annot : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list
+val ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list
+val collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list
 
-type 'a bFormula = ('a, __, unit0, unit0) gFormula
+type rtyp = __
+type eKind = __
+type 'a bFormula = ('a, eKind, unit0, unit0) gFormula
 
 val map_bformula :
-  ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5) gFormula
+     kind
+  -> ('a1 -> 'a2)
+  -> ('a1, 'a3, 'a4, 'a5) gFormula
+  -> ('a2, 'a3, 'a4, 'a5) gFormula
 
 type ('x, 'annot) clause = ('x * 'annot) list
 type ('x, 'annot) cnf = ('x, 'annot) clause list
@@ -334,12 +351,55 @@ val or_cnf_opt :
   -> ('a1, 'a2) cnf
   -> ('a1, 'a2) cnf
 
+val mk_and :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf)
+  -> kind
+  -> bool
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf
+
+val mk_or :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf)
+  -> kind
+  -> bool
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf
+
+val mk_impl :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf)
+  -> kind
+  -> bool
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf
+
+val mk_iff :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf)
+  -> kind
+  -> bool
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf
+
+val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option
+
 val xcnf :
      ('a2 -> bool)
   -> ('a2 -> 'a2 -> 'a2 option)
   -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
   -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
   -> bool
+  -> kind
   -> ('a1, 'a3, 'a4, 'a5) tFormula
   -> ('a2, 'a3) cnf
 
@@ -387,49 +447,199 @@ val ror_cnf_opt :
 
 val ratom : ('a1, 'a2) cnf -> 'a2 -> ('a1, 'a2) cnf * 'a2 list
 
+val rxcnf_and :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (   bool
+      -> kind
+      -> ('a1, 'a3, 'a4, 'a5) tFormula
+      -> ('a2, 'a3) cnf * 'a3 list)
+  -> bool
+  -> kind
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf * 'a3 list
+
+val rxcnf_or :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (   bool
+      -> kind
+      -> ('a1, 'a3, 'a4, 'a5) tFormula
+      -> ('a2, 'a3) cnf * 'a3 list)
+  -> bool
+  -> kind
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf * 'a3 list
+
+val rxcnf_impl :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (   bool
+      -> kind
+      -> ('a1, 'a3, 'a4, 'a5) tFormula
+      -> ('a2, 'a3) cnf * 'a3 list)
+  -> bool
+  -> kind
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf * 'a3 list
+
+val rxcnf_iff :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (   bool
+      -> kind
+      -> ('a1, 'a3, 'a4, 'a5) tFormula
+      -> ('a2, 'a3) cnf * 'a3 list)
+  -> bool
+  -> kind
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf * 'a3 list
+
 val rxcnf :
      ('a2 -> bool)
   -> ('a2 -> 'a2 -> 'a2 option)
   -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
   -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
   -> bool
+  -> kind
   -> ('a1, 'a3, 'a4, 'a5) tFormula
   -> ('a2, 'a3) cnf * 'a3 list
 
 type ('term, 'annot, 'tX) to_constrT =
-  { mkTT : 'tX
-  ; mkFF : 'tX
-  ; mkA : 'term -> 'annot -> 'tX
-  ; mkCj : 'tX -> 'tX -> 'tX
-  ; mkD : 'tX -> 'tX -> 'tX
-  ; mkI : 'tX -> 'tX -> 'tX
-  ; mkN : 'tX -> 'tX }
+  { mkTT : kind -> 'tX
+  ; mkFF : kind -> 'tX
+  ; mkA : kind -> 'term -> 'annot -> 'tX
+  ; mkAND : kind -> 'tX -> 'tX -> 'tX
+  ; mkOR : kind -> 'tX -> 'tX -> 'tX
+  ; mkIMPL : kind -> 'tX -> 'tX -> 'tX
+  ; mkIFF : kind -> 'tX -> 'tX -> 'tX
+  ; mkNOT : kind -> 'tX -> 'tX
+  ; mkEQ : 'tX -> 'tX -> 'tX }
 
 val aformula :
-  ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3
+  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3
 
-val is_X : ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option
+val is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option
 
 val abs_and :
      ('a1, 'a2, 'a3) to_constrT
+  -> kind
   -> ('a1, 'a2, 'a3, 'a4) tFormula
   -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> (   ('a1, 'a2, 'a3, 'a4) tFormula
+  -> (   kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
       -> ('a1, 'a2, 'a3, 'a4) tFormula
       -> ('a1, 'a2, 'a3, 'a4) tFormula)
   -> ('a1, 'a3, 'a2, 'a4) gFormula
 
 val abs_or :
      ('a1, 'a2, 'a3) to_constrT
+  -> kind
   -> ('a1, 'a2, 'a3, 'a4) tFormula
   -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> (   ('a1, 'a2, 'a3, 'a4) tFormula
+  -> (   kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
       -> ('a1, 'a2, 'a3, 'a4) tFormula
       -> ('a1, 'a2, 'a3, 'a4) tFormula)
   -> ('a1, 'a3, 'a2, 'a4) gFormula
 
+val abs_not :
+     ('a1, 'a2, 'a3) to_constrT
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula)
+  -> ('a1, 'a3, 'a2, 'a4) gFormula
+
 val mk_arrow :
      'a4 option
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val abst_simpl :
+     ('a1, 'a2, 'a3) to_constrT
+  -> ('a2 -> bool)
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val abst_and :
+     ('a1, 'a2, 'a3) to_constrT
+  -> (   bool
+      -> kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
+      -> ('a1, 'a2, 'a3, 'a4) tFormula)
+  -> bool
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val abst_or :
+     ('a1, 'a2, 'a3) to_constrT
+  -> (   bool
+      -> kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
+      -> ('a1, 'a2, 'a3, 'a4) tFormula)
+  -> bool
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val abst_impl :
+     ('a1, 'a2, 'a3) to_constrT
+  -> (   bool
+      -> kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
+      -> ('a1, 'a2, 'a3, 'a4) tFormula)
+  -> bool
+  -> 'a4 option
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val or_is_X :
+  kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool
+
+val abs_iff :
+     ('a1, 'a2, 'a3) to_constrT
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val abst_iff :
+     ('a1, 'a2, 'a3) to_constrT
+  -> ('a2 -> bool)
+  -> (   bool
+      -> kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
+      -> ('a1, 'a2, 'a3, 'a4) tFormula)
+  -> bool
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val abst_eq :
+     ('a1, 'a2, 'a3) to_constrT
+  -> ('a2 -> bool)
+  -> (   bool
+      -> kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
+      -> ('a1, 'a2, 'a3, 'a4) tFormula)
+  -> bool
   -> ('a1, 'a2, 'a3, 'a4) tFormula
   -> ('a1, 'a2, 'a3, 'a4) tFormula
   -> ('a1, 'a2, 'a3, 'a4) tFormula
@@ -438,8 +648,9 @@ val abst_form :
      ('a1, 'a2, 'a3) to_constrT
   -> ('a2 -> bool)
   -> bool
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
   -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a3, 'a2, 'a4) gFormula
 
 val cnf_checker :
   (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool
@@ -450,7 +661,7 @@ val tauto_checker :
   -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
   -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
   -> (('a2 * 'a3) list -> 'a4 -> bool)
-  -> ('a1, __, 'a3, unit0) gFormula
+  -> ('a1, rtyp, 'a3, unit0) gFormula
   -> 'a4 list
   -> bool
 
@@ -661,7 +872,9 @@ val xnegate0 : z nFormula -> z nFormula list
 val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf
 
 val cnfZ :
-  (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list
+     kind
+  -> (z formula, 'a1, 'a2, 'a3) tFormula
+  -> (z nFormula, 'a1) cnf * 'a1 list
 
 val ceiling : z -> z -> z
 
@@ -698,7 +911,9 @@ val qdeduce : q nFormula -> q nFormula -> q nFormula option
 val normQ : q pExpr -> q pol
 
 val cnfQ :
-  (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 list
+     kind
+  -> (q formula, 'a1, 'a2, 'a3) tFormula
+  -> (q nFormula, 'a1) cnf * 'a1 list
 
 val qTautoChecker : q formula bFormula -> qWitness list -> bool
 
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 41579d5792..fa7b4aa480 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -248,10 +248,12 @@ module EBinOpT = struct
       source1 : EConstr.t
     ; source2 : EConstr.t
     ; source3 : EConstr.t
-    ; target : EConstr.t
-    ; inj1 : EInjT.t (* InjTyp source1 target *)
-    ; inj2 : EInjT.t (* InjTyp source2 target *)
-    ; inj3 : EInjT.t (* InjTyp source3 target *)
+    ; target1 : EConstr.t
+    ; target2 : EConstr.t
+    ; target3 : EConstr.t
+    ; inj1 : EInjT.t (* InjTyp source1 target1 *)
+    ; inj2 : EInjT.t (* InjTyp source2 target2 *)
+    ; inj3 : EInjT.t (* InjTyp source3 target3 *)
     ; bop : EConstr.t (* BOP *)
     ; tbop : EConstr.t (* TBOP *)
     ; tbopinj : EConstr.t (* TBOpInj *)
@@ -272,7 +274,8 @@ module EUnOpT = struct
   type t =
     { source1 : EConstr.t
     ; source2 : EConstr.t
-    ; target : EConstr.t
+    ; target1 : EConstr.t
+    ; target2 : EConstr.t
     ; uop : EConstr.t
     ; inj1_t : EInjT.t
     ; inj2_t : EInjT.t
@@ -392,24 +395,26 @@ module EBinOp = struct
   let table = table
 
   let mk_elt evd i a =
-    let i1 = get_inj evd a.(5) in
-    let i2 = get_inj evd a.(6) in
-    let i3 = get_inj evd a.(7) in
-    let tbop = a.(8) in
+    let i1 = get_inj evd a.(7) in
+    let i2 = get_inj evd a.(8) in
+    let i3 = get_inj evd a.(9) in
+    let tbop = a.(10) in
     { source1 = a.(0)
     ; source2 = a.(1)
     ; source3 = a.(2)
-    ; target = a.(3)
+    ; target1 = a.(3)
+    ; target2 = a.(4)
+    ; target3 = a.(5)
     ; inj1 = i1
     ; inj2 = i2
     ; inj3 = i3
-    ; bop = a.(4)
-    ; tbop = a.(8)
-    ; tbopinj = a.(9)
+    ; bop = a.(6)
+    ; tbop
+    ; tbopinj = a.(11)
     ; classify_binop =
-        classify_op (mkconvert_binop i1 i2 i3) i1.EInjT.inj a.(4) tbop }
+        classify_op (mkconvert_binop i1 i2 i3) i3.EInjT.inj a.(6) tbop }
 
-  let get_key = 4
+  let get_key = 6
   let cast x = BinOp x
   let dest = function BinOp x -> Some x | _ -> None
 end
@@ -452,23 +457,24 @@ module EUnOp = struct
   let dest = function UnOp x -> Some x | _ -> None
 
   let mk_elt evd i a =
-    let i1 = get_inj evd a.(4) in
-    let i2 = get_inj evd a.(5) in
-    let uop = a.(3) in
-    let tuop = a.(6) in
+    let i1 = get_inj evd a.(5) in
+    let i2 = get_inj evd a.(6) in
+    let uop = a.(4) in
+    let tuop = a.(7) in
     { source1 = a.(0)
     ; source2 = a.(1)
-    ; target = a.(2)
+    ; target1 = a.(2)
+    ; target2 = a.(3)
     ; uop
     ; inj1_t = i1
     ; inj2_t = i2
     ; tuop
-    ; tuopinj = a.(7)
+    ; tuopinj = a.(8)
     ; is_construct = EConstr.isConstruct evd uop
-    ; classify_unop = classify_op (mkconvert_unop i1 i2) i1.EInjT.inj uop tuop
+    ; classify_unop = classify_op (mkconvert_unop i1 i2) i2.EInjT.inj uop tuop
     }
 
-  let get_key = 3
+  let get_key = 4
 end
 
 module EBinRel = struct
@@ -788,7 +794,8 @@ let app_unop evd src unop arg prf =
             ( force mkapp
             , [| unop.source1
                ; unop.source2
-               ; unop.target
+               ; unop.target1
+               ; unop.target2
                ; unop.uop
                ; unop.inj1_t.EInjT.inj
                ; unop.inj2_t.EInjT.inj
@@ -859,7 +866,9 @@ let app_binop evd src binop arg1 prf1 arg2 prf2 =
             , [| binop.source1
                ; binop.source2
                ; binop.source3
-               ; binop.target
+               ; binop.target1
+               ; binop.target2
+               ; binop.target3
                ; binop.bop
                ; binop.inj1.EInjT.inj
                ; binop.inj2.EInjT.inj