formatting

8 files changed, 497 insertions, 509 deletions

diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 832778a..72e7ed3 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -133,33 +133,33 @@ module Btype =
 
 (** Operators *)
 
-type cop = 
-   | CO_xH
-   | CO_Z0
+type cop =
+  | CO_xH
+  | CO_Z0
 
 type uop =
-   | UO_xO
-   | UO_xI
-   | UO_Zpos 
-   | UO_Zneg
-   | UO_Zopp
-
-type bop = 
-   | BO_Zplus
-   | BO_Zminus
-   | BO_Zmult
-   | BO_Zlt
-   | BO_Zle
-   | BO_Zge
-   | BO_Zgt
-   | BO_eq of btype
+  | UO_xO
+  | UO_xI
+  | UO_Zpos
+  | UO_Zneg
+  | UO_Zopp
+
+type bop =
+  | BO_Zplus
+  | BO_Zminus
+  | BO_Zmult
+  | BO_Zlt
+  | BO_Zle
+  | BO_Zge
+  | BO_Zgt
+  | BO_eq of btype
 
 type nop =
   | NO_distinct of btype
 
-type op_def = { 
-    tparams : btype array; 
-    tres : btype; 
+type op_def = {
+    tparams : btype array;
+    tres : btype;
     op_val : Term.constr }
 
 type indexed_op = op_def gen_hashed 
@@ -175,7 +175,7 @@ type op =
   | Iop of indexed_op
 
 module Op =
-  struct 
+  struct
     let c_to_coq = function
       | CO_xH -> Lazy.force cCO_xH
       | CO_Z0 -> Lazy.force cCO_Z0
@@ -188,18 +188,18 @@ module Op =
       | CO_xH -> Lazy.force cxH
       | CO_Z0 -> Lazy.force cZ0
 
-    let u_to_coq = function 
+    let u_to_coq = function
       | UO_xO -> Lazy.force cUO_xO
       | UO_xI -> Lazy.force cUO_xI
-      | UO_Zpos -> Lazy.force cUO_Zpos 
+      | UO_Zpos -> Lazy.force cUO_Zpos
       | UO_Zneg -> Lazy.force cUO_Zneg
       | UO_Zopp -> Lazy.force cUO_Zopp
 
-    let u_type_of = function 
+    let u_type_of = function
       | UO_xO | UO_xI -> Tpositive
       | UO_Zpos | UO_Zneg | UO_Zopp -> TZ
 
-    let u_type_arg = function 
+    let u_type_arg = function
       | UO_xO | UO_xI | UO_Zpos | UO_Zneg -> Tpositive
       | UO_Zopp -> TZ
 
@@ -210,15 +210,15 @@ module Op =
       | UO_Zneg -> Lazy.force cZneg
       | UO_Zopp -> Lazy.force copp
 
-    let eq_tbl = Hashtbl.create 17 
+    let eq_tbl = Hashtbl.create 17
 
     let eq_to_coq t =
-      try Hashtbl.find eq_tbl t 
+      try Hashtbl.find eq_tbl t
       with Not_found ->
 	let op = mklApp cBO_eq [|Btype.to_coq t|] in
 	Hashtbl.add eq_tbl t op;
 	op
-     
+
     let b_to_coq = function
       | BO_Zplus -> Lazy.force cBO_Zplus
       | BO_Zminus -> Lazy.force cBO_Zminus
@@ -277,14 +277,14 @@ module Op =
     let i_type_of i = i.hval.tres
 
     let i_type_args i = i.hval.tparams
-	  
+
     (* reify table *)
     type reify_tbl =
-        { mutable count : int;
-	          tbl : (Term.constr, indexed_op) Hashtbl.t
-	}
+      { mutable count : int;
+	        tbl : (Term.constr, indexed_op) Hashtbl.t
+      }
 
-    let create () = 
+    let create () =
       { count = 0;
 	tbl =  Hashtbl.create 17 }
 
@@ -301,10 +301,10 @@ module Op =
 
 
     let interp_tbl tval mk_Tval reify =
-      let t = Array.make (reify.count + 1) 
-	  (mk_Tval [||] Tbool (Lazy.force ctrue))  in
-      let set _ v = 
-	t.(v.index) <- mk_Tval v.hval.tparams v.hval.tres v.hval.op_val in
+      let t = Array.make (reify.count + 1)
+	        (mk_Tval [||] Tbool (Lazy.force ctrue)) in
+      let set _ v =
+        t.(v.index) <- mk_Tval v.hval.tparams v.hval.tres v.hval.op_val in
       Hashtbl.iter set reify.tbl;
       Structures.mkArray (tval, t)
 
@@ -320,12 +320,12 @@ module Op =
 
     let b_equal op1 op2 =
       match op1,op2 with
-        | BO_eq t1, BO_eq t2 -> Btype.equal t1 t2
-        | _ -> op1 == op2
+      | BO_eq t1, BO_eq t2 -> Btype.equal t1 t2
+      | _ -> op1 == op2
 
     let n_equal op1 op2 =
       match op1,op2 with
-        | NO_distinct t1, NO_distinct t2 -> Btype.equal t1 t2
+      | NO_distinct t1, NO_distinct t2 -> Btype.equal t1 t2
 
     let i_equal op1 op2 = op1.index == op2.index
 
@@ -334,10 +334,10 @@ module Op =
 
 (** Definition of atoms *)
 
-type atom = 
+type atom =
   | Acop of cop
-  | Auop of uop * hatom 
-  | Abop of bop * hatom * hatom 
+  | Auop of uop * hatom
+  | Abop of bop * hatom * hatom
   | Anop of nop * hatom array
   | Aapp of indexed_op * hatom array
 
@@ -371,7 +371,7 @@ and hatom = atom gen_hashed
 (*   | Aapp (op,a) -> "(Aapp "^(string_of_int op.index)^" ("^(Array.fold_left (fun acc h -> acc^" "^(pp_atom h.hval)) "" a)^"))" *)
 
 module HashedAtom =
-  struct 
+  struct
     type t = atom
 
     let equal a b =
@@ -379,53 +379,53 @@ module HashedAtom =
       | Acop opa, Acop opb -> Op.c_equal opa opb
       | Auop(opa,ha), Auop(opb,hb) -> Op.u_equal opa opb && ha.index == hb.index
       | Abop(opa,ha1,ha2), Abop(opb,hb1,hb2) ->
-	  Op.b_equal opa opb && ha1.index == hb1.index && ha2.index == hb2.index
+	 Op.b_equal opa opb && ha1.index == hb1.index && ha2.index == hb2.index 
       | Anop (opa,ha), Anop (opb,hb) ->
-        let na = Array.length ha in
-        let nb = Array.length hb in
-        let i = ref (-1) in
-        Op.n_equal opa opb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha
+         let na = Array.length ha in
+         let nb = Array.length hb in
+         let i = ref (-1) in
+         Op.n_equal opa opb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha
       | Aapp (va,ha), Aapp (vb,hb) ->
-        let na = Array.length ha in
-        let nb = Array.length hb in
-        let i = ref (-1) in
-        Op.i_equal va vb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha
+         let na = Array.length ha in
+         let nb = Array.length hb in
+         let i = ref (-1) in
+         Op.i_equal va vb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha
       | _, _ -> false
 
     let hash = function
       |	Acop op -> ((Hashtbl.hash op) lsl 3) lxor 1
       | Auop (op,h) ->
-          (( (h.index lsl 3) + (Hashtbl.hash op)) lsl 3) lxor 2
+         (( (h.index lsl 3) + (Hashtbl.hash op)) lsl 3) lxor 2
       | Abop (op,h1,h2) ->
-          (((( (h1.index lsl 2) + h2.index) lsl 3) + Hashtbl.hash op) lsl 3) lxor 3
+         (((( (h1.index lsl 2) + h2.index) lsl 3) + Hashtbl.hash op) lsl 3) lxor 3
       | Anop (op, args) ->
-          let hash_args =
-            match Array.length args with
-            | 0 -> 0
-            | 1 -> args.(0).index
-            | 2 -> args.(1).index lsl 2 + args.(0).index
-            | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in
-          (hash_args lsl 5 + (Hashtbl.hash op) lsl 3) lxor 4
+         let hash_args =
+           match Array.length args with
+           | 0 -> 0
+           | 1 -> args.(0).index
+           | 2 -> args.(1).index lsl 2 + args.(0).index
+           | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in
+         (hash_args lsl 5 + (Hashtbl.hash op) lsl 3) lxor 4
       | Aapp (op, args) ->
-          let hash_args =
-            match Array.length args with
-            | 0 -> 0
-            | 1 -> args.(0).index
-            | 2 -> args.(1).index lsl 2 + args.(0).index
-            | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in
-          (hash_args lsl 5 + op.index lsl 3) lxor 4
+         let hash_args =
+           match Array.length args with
+           | 0 -> 0
+           | 1 -> args.(0).index
+           | 2 -> args.(1).index lsl 2 + args.(0).index
+           | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in
+         (hash_args lsl 5 + op.index lsl 3) lxor 4
 
   end
 
 module HashAtom = Hashtbl.Make(HashedAtom)
 
-module Atom = 
-  struct 
+module Atom =
+  struct
 
     type t = hatom
 
     let atom h = h.hval
-    let index h = h.index 
+    let index h = h.index
 
     let equal h1 h2 = h1.index == h2.index
 
@@ -442,11 +442,11 @@ module Atom =
 
     let rec compute_int = function
       | Acop c ->
-        (match c with
+         (match c with
           | CO_xH -> 1
           | CO_Z0 -> 0)
       | Auop (op,h) ->
-        (match op with
+         (match op with
           | UO_xO -> 2*(compute_hint h)
           | UO_xI -> 2*(compute_hint h) + 1
           | UO_Zpos -> compute_hint h
@@ -464,46 +464,46 @@ module Atom =
 
     let rec to_smt fmt h = to_smt_atom fmt (atom h)
 
-    and to_smt_atom fmt = function
-      | Acop _ as a -> to_smt_int fmt (compute_int a)
-      | Auop (UO_Zopp,h) ->
-        Format.fprintf fmt "(- ";
-        to_smt fmt h;
-        Format.fprintf fmt ")"
-      | Auop _ as a -> to_smt_int fmt (compute_int a)
-      | Abop (op,h1,h2) -> to_smt_bop fmt op h1 h2
-      | Anop (op,a) -> to_smt_nop fmt op a
-      | Aapp (op,a) ->
-        if Array.length a = 0 then (
-          Format.fprintf fmt "op_%i" op.index;
-        ) else (
-          Format.fprintf fmt "(op_%i" op.index;
-          Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a;
+      and to_smt_atom fmt = function
+        | Acop _ as a -> to_smt_int fmt (compute_int a)
+        | Auop (UO_Zopp,h) ->
+          Format.fprintf fmt "(- ";
+          to_smt fmt h;
           Format.fprintf fmt ")"
-        )
-
-    and to_smt_bop fmt op h1 h2 =
-      let s = match op with
-        | BO_Zplus -> "+"
-        | BO_Zminus -> "-"
-        | BO_Zmult -> "*"
-        | BO_Zlt -> "<"
-        | BO_Zle -> "<="
-        | BO_Zge -> ">="
-        | BO_Zgt -> ">"
-        | BO_eq _ -> "=" in
-      Format.fprintf fmt "(%s " s;
-      to_smt fmt h1;
-      Format.fprintf fmt " ";
-      to_smt fmt h2;
-      Format.fprintf fmt ")"
-
-    and to_smt_nop fmt op a =
-      let s = match op with
-        | NO_distinct _ -> "distinct" in
-      Format.fprintf fmt "(%s" s;
-      Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a;
-      Format.fprintf fmt ")"
+        | Auop _ as a -> to_smt_int fmt (compute_int a)
+        | Abop (op,h1,h2) -> to_smt_bop fmt op h1 h2
+        | Anop (op,a) -> to_smt_nop fmt op a
+        | Aapp (op,a) ->
+          if Array.length a = 0 then (
+            Format.fprintf fmt "op_%i" op.index;
+          ) else (
+            Format.fprintf fmt "(op_%i" op.index;
+            Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a;
+            Format.fprintf fmt ")"
+          )
+
+      and to_smt_bop fmt op h1 h2 =
+        let s = match op with
+          | BO_Zplus -> "+"
+          | BO_Zminus -> "-"
+          | BO_Zmult -> "*"
+          | BO_Zlt -> "<"
+          | BO_Zle -> "<="
+          | BO_Zge -> ">="
+          | BO_Zgt -> ">"
+          | BO_eq _ -> "=" in
+        Format.fprintf fmt "(%s " s;
+        to_smt fmt h1;
+        Format.fprintf fmt " ";
+        to_smt fmt h2;
+        Format.fprintf fmt ")"
+
+      and to_smt_nop fmt op a =
+        let s = match op with
+          | NO_distinct _ -> "distinct" in
+        Format.fprintf fmt "(%s" s;
+        Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a;
+        Format.fprintf fmt ")"
 
 
 
@@ -512,28 +512,29 @@ module Atom =
     let check a =
       match a with
       | Acop _ -> ()
-      | Auop(op,h) -> 
-	  if not (Btype.equal (Op.u_type_arg op) (type_of h)) then
-	    raise (NotWellTyped a)
+      | Auop(op,h) ->
+	 if not (Btype.equal (Op.u_type_arg op) (type_of h))
+         then raise (NotWellTyped a)
       | Abop(op,h1,h2) ->
-	  let (t1,t2) = Op.b_type_args op in
-	  if not (Btype.equal t1 (type_of h1) && Btype.equal t2 (type_of h2))
-	  then raise (NotWellTyped a)
+	 let (t1,t2) = Op.b_type_args op in
+	 if not (Btype.equal t1 (type_of h1) && Btype.equal t2 (type_of h2))
+	 then raise (NotWellTyped a)
       | Anop(op,ha) ->
-        let ty = Op.n_type_args op in
-        Array.iter (fun h -> if not (Btype.equal ty (type_of h)) then raise (NotWellTyped a)) ha
+         let ty = Op.n_type_args op in
+         Array.iter (fun h -> if not (Btype.equal ty (type_of h)) then raise (NotWellTyped a)) ha
       | Aapp(op,args) ->
-	  let tparams = Op.i_type_args op in
-	  Array.iteri (fun i t -> 
-	    if not (Btype.equal t (type_of args.(i))) then
-		raise (NotWellTyped a)) tparams
+	 let tparams = Op.i_type_args op in
+	 Array.iteri (fun i t ->
+	     if not (Btype.equal t (type_of args.(i))) then
+	       raise (NotWellTyped a)) tparams
 
     type reify_tbl =
-        { mutable count : int;
-	          tbl : hatom HashAtom.t 
-	}
+      { mutable count : int;
+	        tbl : hatom HashAtom.t
+      }
 
-    let create () = 
+
+    let create () =
       { count = 0;
 	tbl =  HashAtom.create 17 }
 
@@ -541,7 +542,7 @@ module Atom =
       reify.count <- 0;
       HashAtom.clear reify.tbl
 
-    let declare reify a = 
+    let declare reify a =
       check a;
       let res = {index = reify.count; hval = a} in
       HashAtom.add reify.tbl a res;
@@ -549,7 +550,7 @@ module Atom =
       res
 
     let get reify a =
-      try HashAtom.find reify.tbl a 
+      try HashAtom.find reify.tbl a
       with Not_found -> declare reify a
 
 
@@ -594,26 +595,26 @@ module Atom =
 	try Hashtbl.find op_tbl c with Not_found -> CCunknown in
       let mk_cop op = get reify (Acop op) in
       let rec mk_hatom h =
-	let c, args = Term.decompose_app h in
+        let c, args = Term.decompose_app h in
 	match get_cst c with
-          | CCxH -> mk_cop CO_xH
-          | CCZ0 -> mk_cop CO_Z0
-          | CCxO -> mk_uop UO_xO args
-          | CCxI -> mk_uop UO_xI args
-          | CCZpos -> mk_uop UO_Zpos args
-          | CCZneg -> mk_uop UO_Zneg args
-          | CCZopp -> mk_uop UO_Zopp args
-          | CCZplus -> mk_bop BO_Zplus args
-          | CCZminus -> mk_bop BO_Zminus args
-          | CCZmult -> mk_bop BO_Zmult args
-          | CCZlt -> mk_bop BO_Zlt args
-          | CCZle -> mk_bop BO_Zle args
-          | CCZge -> mk_bop BO_Zge args
-          | CCZgt -> mk_bop BO_Zgt args
-          | CCeqb -> mk_bop (BO_eq Tbool) args
-          | CCeqbP -> mk_bop (BO_eq Tpositive) args
-          | CCeqbZ -> mk_bop (BO_eq TZ) args
-	  | CCunknown -> mk_unknown c args (Retyping.get_type_of env sigma h)
+        | CCxH -> mk_cop CO_xH
+        | CCZ0 -> mk_cop CO_Z0
+        | CCxO -> mk_uop UO_xO args
+        | CCxI -> mk_uop UO_xI args
+        | CCZpos -> mk_uop UO_Zpos args
+        | CCZneg -> mk_uop UO_Zneg args
+        | CCZopp -> mk_uop UO_Zopp args
+        | CCZplus -> mk_bop BO_Zplus args
+        | CCZminus -> mk_bop BO_Zminus args
+        | CCZmult -> mk_bop BO_Zmult args
+        | CCZlt -> mk_bop BO_Zlt args
+        | CCZle -> mk_bop BO_Zle args
+        | CCZge -> mk_bop BO_Zge args
+        | CCZgt -> mk_bop BO_Zgt args
+        | CCeqb -> mk_bop (BO_eq Tbool) args
+        | CCeqbP -> mk_bop (BO_eq Tpositive) args
+        | CCeqbZ -> mk_bop (BO_eq TZ) args
+	| CCunknown -> mk_unknown c args (Retyping.get_type_of env sigma h)
 
       and mk_uop op = function
         | [a] -> let h = mk_hatom a in get reify (Auop (op,h))
@@ -621,22 +622,21 @@ module Atom =
 
       and mk_bop op = function
         | [a1;a2] ->
-          let h1 = mk_hatom a1 in
-          let h2 = mk_hatom a2 in
-          get reify (Abop (op,h1,h2))
+           let h1 = mk_hatom a1 in
+           let h2 = mk_hatom a2 in
+           get reify (Abop (op,h1,h2))
         | _ -> assert false
 
       and mk_unknown c args ty =
         let hargs = Array.of_list (List.map mk_hatom args) in
-        let op =
-          try Op.of_coq ro c
-          with | Not_found ->
-            let targs = Array.map type_of hargs in
-            let tres = Btype.of_coq rt ty in
-            Op.declare ro c targs tres in
+        let op = try Op.of_coq ro c
+                 with Not_found ->
+                   let targs = Array.map type_of hargs in
+                   let tres = Btype.of_coq rt ty in
+                   Op.declare ro c targs tres in
         get reify (Aapp (op,hargs)) in
 
-       mk_hatom c
+      mk_hatom c
 
 
     let to_coq h = mkInt h.index
@@ -645,16 +645,16 @@ module Atom =
       match a with
       | Acop op -> mklApp cAcop [|Op.c_to_coq op|]
       | Auop (op,h) -> mklApp cAuop [|Op.u_to_coq op; to_coq h|]
-      | Abop (op,h1,h2) -> 
-	  mklApp cAbop [|Op.b_to_coq op;to_coq h1; to_coq h2|]
+      | Abop (op,h1,h2) ->
+	 mklApp cAbop [|Op.b_to_coq op;to_coq h1; to_coq h2|]
       | Anop (op,ha) ->
-        let cop = Op.n_to_coq op in
-        let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) ha (mklApp cnil [|Lazy.force cint|]) in
-        mklApp cAnop [|cop; cargs|]
+         let cop = Op.n_to_coq op in
+         let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) ha (mklApp cnil [|Lazy.force cint|]) in
+         mklApp cAnop [|cop; cargs|]
       | Aapp (op,args) ->
-        let cop = Op.i_to_coq op in
-        let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) args (mklApp cnil [|Lazy.force cint|]) in
-        mklApp cAapp [|cop; cargs|]
+         let cop = Op.i_to_coq op in
+         let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) args (mklApp cnil [|Lazy.force cint|]) in
+         mklApp cAapp [|cop; cargs|]
 
     let dft_atom = lazy (mklApp cAcop [| Lazy.force cCO_xH |])
 
@@ -677,15 +677,15 @@ module Atom =
 	with Not_found ->
 	  let pc =
 	    match atom a with
-              | Acop c -> Op.interp_cop c
-              | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|])
-              | Abop (op,h1,h2) -> Term.mkApp (Op.interp_bop op, [|interp_atom h1; interp_atom h2|])
-              | Anop (NO_distinct ty as op,ha) ->
-                let cop = Op.interp_nop op in
-                let typ = Op.interp_distinct ty in
-                let cargs = Array.fold_right (fun h l -> mklApp ccons [|typ; interp_atom h; l|]) ha (mklApp cnil [|typ|]) in
-                Term.mkApp (cop,[|cargs|])
-              | Aapp (op,t) -> Term.mkApp (op.hval.op_val, Array.map interp_atom t) in
+            | Acop c -> Op.interp_cop c
+            | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|])
+            | Abop (op,h1,h2) -> Term.mkApp (Op.interp_bop op, [|interp_atom h1; interp_atom h2|])
+            | Anop (NO_distinct ty as op,ha) ->
+               let cop = Op.interp_nop op in
+               let typ = Op.interp_distinct ty in
+               let cargs = Array.fold_right (fun h l -> mklApp ccons [|typ; interp_atom h; l|]) ha (mklApp cnil [|typ|]) in
+               Term.mkApp (cop,[|cargs|])
+            | Aapp (op,t) -> Term.mkApp (op.hval.op_val, Array.map interp_atom t) in
 	  Hashtbl.add atom_tbl l pc;
 	  pc in
       interp_atom a
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index cdcdcd1..e6a3c47 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -142,8 +142,8 @@ module Atom :
       val get : reify_tbl -> atom -> hatom
 
       (** Given a coq term, build the corresponding atom *)
-      val of_coq : Btype.reify_tbl -> Op.reify_tbl -> reify_tbl ->
-        Environ.env -> Evd.evar_map -> Term.constr -> t
+      val of_coq : Btype.reify_tbl -> Op.reify_tbl ->
+        reify_tbl -> Environ.env -> Evd.evar_map -> Term.constr -> t
 
       val to_coq : hatom -> Term.constr
 
@@ -157,6 +157,7 @@ module Atom :
       (* Generation of atoms *)
       val hatom_Z_of_int : reify_tbl -> int -> hatom
       val hatom_Z_of_bigint : reify_tbl -> Big_int.big_int -> hatom
+
       val mk_eq : reify_tbl -> btype -> hatom -> hatom -> hatom
       val mk_lt : reify_tbl -> hatom -> hatom -> hatom
       val mk_le : reify_tbl -> hatom -> hatom -> hatom
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index e4ed262..a0972d4 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -21,18 +21,18 @@ type used = int
 type clause_id  = int
 
 type 'hform rule =
-  | ImmFlatten of 'hform clause * 'hform 
+  | ImmFlatten of 'hform clause * 'hform
 
   (* CNF Transformations *)
-  | True       
-     (*  * true             : {true} 
+  | True
+     (*  * true             : {true}
      *)
-  | False 
-     (* * false             : {(not false)} 
+  | False
+     (* * false             : {(not false)}
      *)
-  | BuildDef of 'hform (* the first literal of the clause *)       
+  | BuildDef of 'hform (* the first literal of the clause *)
      (*  * and_neg          : {(and a_1 ... a_n) (not a_1) ... (not a_n)}
-         * or_pos           : {(not (or a_1 ... a_n)) a_1 ... a_n} 
+         * or_pos           : {(not (or a_1 ... a_n)) a_1 ... a_n}
          * implies_pos      : {(not (implies a b)) (not a) b}
          * xor_pos1         : {(not (xor a b)) a b}
          * xor_neg1         : {(xor a b) a (not b)}
@@ -41,7 +41,7 @@ type 'hform rule =
          * ite_pos1         : {(not (if_then_else a b c)) a c}
          * ite_neg1         : {(if_then_else a b c) a (not c)}
      *)
-  | BuildDef2 of 'hform (* the first literal of the clause *) 
+  | BuildDef2 of 'hform (* the first literal of the clause *)
      (* * xor_pos2          : {(not (xor a b)) (not a) (not b)}
         * xor_neg2          : {(xor a b) (not a) b}
         * equiv_pos2        : {(not (iff a b)) (not a) b}
@@ -50,15 +50,15 @@ type 'hform rule =
         * ite_neg2          : {(if_then_else a b c) (not a) (not b)}
 
      *)
-  | BuildProj of 'hform * int 
+  | BuildProj of 'hform * int
      (*  * or_neg           : {(or a_1 ... a_n) (not a_i)}
-         * and_pos          : {(not (and a_1 ... a_n)) a_i} 
+         * and_pos          : {(not (and a_1 ... a_n)) a_i}
          * implies_neg1     : {(implies a b) a}
          * implies_neg2     : {(implies a b) (not b)}
      *)
 
   (* Immediate CNF transformation : CNF transformation + Reso *)
-  | ImmBuildDef of 'hform clause 
+  | ImmBuildDef of 'hform clause
      (* * not_and           : {(not (and a_1 ... a_n))} --> {(not a_1) ... (not a_n)}
         * or                : {(or a_1 ... a_n)} --> {a_1 ... a_n}
         * implies           : {(implies a b)} --> {(not a) b}
@@ -78,7 +78,7 @@ type 'hform rule =
         * not_ite2          : {(not (if_then_else a b c))} --> {(not a) (not b)}
      *)
   | ImmBuildProj of 'hform clause * int
-     (*  * and               : {(and a_1 ... a_n)} --> {a_i} 
+     (*  * and               : {(and a_1 ... a_n)} --> {a_i}
          * not_or            : {(not (or a_1 ... a_n))} --> {(not a_i)}
          * not_implies1      : {(not (implies a b))} --> {a}
          * not_implies2      : {(not (implies a b))} --> {(not b)}
@@ -90,11 +90,11 @@ type 'hform rule =
         * eq_transitive    : {(not (= x_1 x_2)) ... (not (= x_{n-1} x_n)) (= x_1 x_n)}
     *)
   | EqCgr of 'hform * ('hform option) list
-    (*  * eq_congruent     : {(not (= x_1 y_1)) ... (not (= x_n y_n)) 
+    (*  * eq_congruent     : {(not (= x_1 y_1)) ... (not (= x_n y_n))
                                    (= (f x_1 ... x_n) (f y_1 ... y_n))}
     *)
   | EqCgrP of 'hform * 'hform * ('hform option) list
-    (*  * eq_congruent_pred : {(not (= x_1 y_1)) ... (not (= x_n y_n)) 
+    (*  * eq_congruent_pred : {(not (= x_1 y_1)) ... (not (= x_n y_n))
                                    (not (p x_1 ... x_n)) (p y_1 ... y_n)}
     *)
 
diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli
index dee465c..767dc8b 100644
--- a/src/trace/smtCertif.mli
+++ b/src/trace/smtCertif.mli
@@ -20,14 +20,15 @@ type 'hform rule =
       Structures.Micromega_plugin_Certificate.Mc.zArithProof list
   | SplDistinctElim of 'hform clause * 'hform
   | Hole of 'hform clause list * 'hform list
+
 and 'hform clause = {
-  id : clause_id;
-  mutable kind : 'hform clause_kind;
-  mutable pos : int option;
-  mutable used : used;
-  mutable prev : 'hform clause option;
-  mutable next : 'hform clause option;
-  value : 'hform list option;
+            id    : clause_id;
+    mutable kind  : 'hform clause_kind;
+    mutable pos   : int option;
+    mutable used  : used;
+    mutable prev  : 'hform clause option;
+    mutable next  : 'hform clause option;
+            value : 'hform list option;
 }
 and 'hform clause_kind =
     Root
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index d8ec105..8950022 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -39,7 +39,6 @@ let cchecker_eq_correct =
   gen_constant euf_checker_modules "checker_eq_correct"
 let cchecker_eq = gen_constant euf_checker_modules "checker_eq"
 
-
 (* Given an SMT-LIB2 file and a certif, build the corresponding objects *)
 
 let compute_roots roots last_root =
@@ -387,12 +386,11 @@ let core_tactic call_solver rt ro ra rf env sigma concl =
   let cuts = (Btype.get_cuts rt)@cuts in
 
   List.fold_right (fun (eqn, eqt) tac ->
-      Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac
-    ) cuts
-      (Structures.tclTHEN
-         (Structures.set_evars_tac body_nocast)
-         (Structures.vm_cast_no_check body_cast))
-
+      Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac)
+    cuts
+    (Structures.tclTHEN
+       (Structures.set_evars_tac body_nocast)
+       (Structures.vm_cast_no_check body_cast))
 
 let tactic call_solver rt ro ra rf =
   Structures.tclTHEN
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 1abea36..069f2ec 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -18,17 +18,17 @@ open Util
 open SmtMisc
 open CoqTerms
 
-module type ATOM = 
-  sig 
+module type ATOM =
+  sig
 
-    type t 
+    type t
     val index : t -> int
 
     val equal : t -> t -> bool
 
     val is_bool_type : t -> bool
 
-  end 
+  end
 
 
 type fop =
@@ -42,80 +42,80 @@ type fop =
   | Fite
   | Fnot2 of int
 
-type ('a,'f) gen_pform = 
+type ('a,'f) gen_pform =
   | Fatom of 'a
   | Fapp of fop * 'f array
 
 
 module type FORM =
-  sig 
-    type hatom 
+  sig
+    type hatom
     type t
     type pform = (hatom, t) gen_pform
 
-      val pform_true : pform
-      val pform_false : pform
+    val pform_true : pform
+    val pform_false : pform
 
-      val equal : t -> t -> bool
+    val equal : t -> t -> bool
 
-      val to_lit : t -> int
-      val index : t -> int
-      val pform : t -> pform
+    val to_lit : t -> int
+    val index : t -> int
+    val pform : t -> pform
 
-      val neg : t -> t
-      val is_pos : t -> bool
-      val is_neg : t -> bool
+    val neg : t -> t
+    val is_pos : t -> bool
+    val is_neg : t -> bool
 
       val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
 
-      (* Building formula from positive formula *)
-      exception NotWellTyped of pform
-      type reify 
-      val create : unit -> reify 
-      val clear : reify -> unit
-      val get : reify -> pform -> t
-      
-      (** Give a coq term, build the corresponding formula *)  
-      val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
-   
-      (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
-      val flatten : reify -> t -> t
-
-      (** Producing Coq terms *) 
-
-      val to_coq : t -> Term.constr
-
-      val pform_tbl : reify -> pform array
-
-      val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
-      val interp_tbl : reify -> Term.constr * Term.constr
-      val nvars : reify -> int 
-      (** Producing a Coq term corresponding to the interpretation 
+    (* Building formula from positive formula *)
+    exception NotWellTyped of pform
+    type reify
+    val create : unit -> reify
+    val clear : reify -> unit
+    val get : reify -> pform -> t
+
+    (** Give a coq term, build the corresponding formula *)
+    val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+
+    (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
+    val flatten : reify -> t -> t
+
+    (** Producing Coq terms *)
+
+    val to_coq : t -> Term.constr
+
+    val pform_tbl : reify -> pform array
+
+    val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
+    val interp_tbl : reify -> Term.constr * Term.constr
+    val nvars : reify -> int
+    (** Producing a Coq term corresponding to the interpretation
           of a formula *)
-      (** [interp_atom] map [hatom] to coq term, it is better if it produce
+    (** [interp_atom] map [hatom] to coq term, it is better if it produce
           shared terms. *)
-      val interp_to_coq : 
-	  (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t -> 
-	    t -> Term.constr
+    val interp_to_coq :
+      (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t ->
+      t -> Term.constr
   end
 
 module Make (Atom:ATOM) =
-  struct 
+  struct
 
-    type hatom = Atom.t 
+    type hatom = Atom.t
 
     type pform = (Atom.t, t) gen_pform
- 
+
     and hpform = pform gen_hashed
-	  
-    and t = 
+
+    and t =
       | Pos of hpform
-      | Neg of hpform 
+      | Neg of hpform
 
     let pform_true = Fapp (Ftrue,[||])
     let pform_false = Fapp (Ffalse,[||])
 
-    let equal h1 h2 = 
+    let equal h1 h2 =
       match h1, h2 with
       | Pos hp1, Pos hp2 -> hp1.index == hp2.index
       | Neg hp1, Neg hp2 -> hp1.index == hp2.index
@@ -132,11 +132,11 @@ module Make (Atom:ATOM) =
     let neg = function
       | Pos hp -> Neg hp
       | Neg hp -> Pos hp
-	    
+
     let is_pos = function
       | Pos _ -> true
       | _ -> false
-	    
+
     let is_neg = function
       | Neg _ -> true
       | _ -> false
@@ -175,63 +175,63 @@ module Make (Atom:ATOM) =
 
 
     module HashedForm =
-      struct 
-	
+      struct
+
 	type t = pform
-	      
-	let equal pf1 pf2 = 
+
+	let equal pf1 pf2 =
 	  match pf1, pf2 with
 	  | Fatom ha1, Fatom ha2 -> Atom.equal ha1 ha2
 	  | Fapp(op1,args1), Fapp(op2,args2) ->
 	      op1 = op2 && 
-	      Array.length args1 == Array.length args2 &&
-	      (try 
-		for i = 0 to Array.length args1 - 1 do
-		  if not (equal args1.(i) args2.(i)) then raise Not_found 
-		done;
-		true
-	      with Not_found -> false)
+	       Array.length args1 == Array.length args2 &&
+	         (try
+		    for i = 0 to Array.length args1 - 1 do
+		      if not (equal args1.(i) args2.(i)) then raise Not_found
+		    done;
+		    true
+	          with Not_found -> false)
 	  | _, _ -> false
 
-	let hash pf = 
+	let hash pf =
 	  match pf with
-	  | Fatom ha1 -> Atom.index ha1 * 2 
-	  | Fapp(op, args) -> 
-	      let hash_args =
-		match Array.length args with
-		| 0 -> 0
-		| 1 -> to_lit args.(0)
-		| 2 -> (to_lit args.(1)) lsl 2 + to_lit args.(0)
-		| _ -> 
-		    (to_lit args.(2)) lsl 4 + (to_lit args.(1)) lsl 2 +
-		      to_lit args.(0) in
-	      (hash_args * 10 + Hashtbl.hash op) * 2 + 1
-		
+	  | Fatom ha1 -> Atom.index ha1 * 2
+	  | Fapp(op, args) ->
+	     let hash_args =
+	       match Array.length args with
+	       | 0 -> 0
+	       | 1 -> to_lit args.(0)
+	       | 2 -> (to_lit args.(1)) lsl 2 + to_lit args.(0)
+	       | _ ->
+		  (to_lit args.(2)) lsl 4 + (to_lit args.(1)) lsl 2 +
+		    to_lit args.(0) in
+	     (hash_args * 10 + Hashtbl.hash op) * 2 + 1
+
       end
 
     module HashForm = Hashtbl.Make (HashedForm)
 
     type reify = {
 	mutable count : int;
-                tbl : t HashForm.t 
-      }  
+                tbl : t HashForm.t
+      }
 
     exception NotWellTyped of pform
-   	
-    let check pf = 
+
+    let check pf =
       match pf with
       | Fatom ha ->  if not (Atom.is_bool_type ha) then raise (NotWellTyped pf)
       | Fapp (op, args) ->
-	  match op with
-	  | Ftrue | Ffalse -> 
-	      if Array.length args <> 0 then raise (NotWellTyped pf)
-	  | Fnot2 _ -> 
-	      if Array.length args <> 1 then raise (NotWellTyped pf)
-	  | Fand | For -> ()
-	  | Fxor | Fimp | Fiff ->
-	      if Array.length args <> 2 then raise (NotWellTyped pf)
-	  | Fite ->
-	      if Array.length args <> 3 then raise (NotWellTyped pf)
+	 match op with
+	 | Ftrue | Ffalse ->
+	    if Array.length args <> 0 then raise (NotWellTyped pf)
+	 | Fnot2 _ ->
+	    if Array.length args <> 1 then raise (NotWellTyped pf)
+	 | Fand | For -> ()
+	 | Fxor | Fimp | Fiff ->
+	    if Array.length args <> 2 then raise (NotWellTyped pf)
+	 | Fite ->
+	    if Array.length args <> 3 then raise (NotWellTyped pf)
 
     let declare reify pf =
       check pf;
@@ -241,8 +241,8 @@ module Make (Atom:ATOM) =
       res
 
     let create () =
-      let reify = 
-	{ count = 0; 
+      let reify =
+	{ count = 0;
 	  tbl =  HashForm.create 17 } in
       let _ = declare reify pform_true in
       let _ = declare reify pform_false in
@@ -256,12 +256,11 @@ module Make (Atom:ATOM) =
       ()
 
     let get reify pf =
-      try HashForm.find reify.tbl pf 
+      try HashForm.find reify.tbl pf
       with Not_found -> declare reify pf
 
-
-    (** Given a coq term, build the corresponding formula *)  
-    type coq_cst = 
+    (** Given a coq term, build the corresponding formula *)
+    type coq_cst =
       | CCtrue
       | CCfalse
       | CCnot
@@ -283,11 +282,11 @@ module Make (Atom:ATOM) =
     let op_tbl () =
       let tbl = ConstrHashtbl.create 29 in
       let add (c1,c2) = ConstrHashtbl.add tbl (Lazy.force c1) c2 in
-      List.iter add 
+      List.iter add
 	[
-	 ctrue,CCtrue; cfalse,CCfalse;
-	 candb,CCand; corb,CCor; cxorb,CCxor; cimplb,CCimp; cnegb,CCnot;
-         ceqb,CCiff; cifb,CCifb ];
+	  ctrue,CCtrue; cfalse,CCfalse;
+	  candb,CCand; corb,CCor; cxorb,CCxor; cimplb,CCimp; cnegb,CCnot;
+          ceqb,CCiff; cifb,CCifb ];
       tbl
 
     let op_tbl = lazy (op_tbl ())
@@ -296,125 +295,124 @@ module Make (Atom:ATOM) =
 
     let of_coq atom_of_coq reify c =
       let op_tbl = Lazy.force op_tbl in
-      let get_cst c = 
-	try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in
+      let get_cst c =
+        try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in
       let rec mk_hform h =
-	let c, args = Term.decompose_app h in
-	match get_cst c with
-	| CCtrue  -> get reify (Fapp(Ftrue,empty_args))
-	| CCfalse -> get reify (Fapp(Ffalse,empty_args))
-	| CCnot -> mk_fnot 1 args
-	| CCand -> mk_fand [] args
-	| CCor  -> mk_for [] args
-	| CCxor -> op2 (fun l -> Fapp(Fxor,l)) args
-	| CCiff -> op2 (fun l -> Fapp(Fiff,l)) args
-	| CCimp ->
-          (match args with
+        let c, args = Term.decompose_app h in
+        match get_cst c with
+        | CCtrue  -> get reify (Fapp(Ftrue,empty_args))
+        | CCfalse -> get reify (Fapp(Ffalse,empty_args))
+        | CCnot -> mk_fnot 1 args
+        | CCand -> mk_fand [] args
+        | CCor  -> mk_for [] args
+        | CCxor -> op2 (fun l -> Fapp(Fxor,l)) args
+        | CCiff -> op2 (fun l -> Fapp(Fiff,l)) args
+        | CCimp ->
+           (match args with
             | [b1;b2] ->
+               let l1 = mk_hform b1 in
+               let l2 = mk_hform b2 in
+               get reify (Fapp (Fimp, [|l1;l2|]))
+            | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb")
+        | CCifb ->
+           (* We should also be able to reify if then else *)
+           begin match args with
+           | [b1;b2;b3] ->
               let l1 = mk_hform b1 in
               let l2 = mk_hform b2 in
-              get reify (Fapp (Fimp, [|l1;l2|]))
-            | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb")
-	| CCifb ->
-	    (* We should also be able to reify if then else *)
-	    begin match args with
-	    | [b1;b2;b3] ->
-		let l1 = mk_hform b1 in
-		let l2 = mk_hform b2 in
-		let l3 = mk_hform b3 in
-		get reify (Fapp(Fite, [|l1;l2;l3|]))
-	    | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
-	    end
-	| _ -> 
-	    let a = atom_of_coq  h in
-            get reify (Fatom a)
+              let l3 = mk_hform b3 in
+              get reify (Fapp (Fite, [|l1;l2;l3|]))
+           | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
+           end
+        | _ ->
+           let a = atom_of_coq h in
+           get reify (Fatom a)
 
       and op2 f args =
-	match args with
-	| [b1;b2] ->
-	    let l1 = mk_hform b1 in
-            let l2 = mk_hform b2 in
-            get reify (f [|l1; l2|])
-	| _ ->  Structures.error "SmtForm.Form.of_coq: wrong number of arguments"
-	  
+        match args with
+        | [b1;b2] ->
+           let l1 = mk_hform b1 in
+           let l2 = mk_hform b2 in
+           get reify (f [|l1; l2|])
+        | _ ->  Structures.error "SmtForm.Form.of_coq: wrong number of arguments"
+
       and mk_fnot i args =
-	match args with
-	| [t] -> 
-	    let c,args = Term.decompose_app t in
-	    if Term.eq_constr c (Lazy.force cnegb) then
-              mk_fnot (i+1) args
-	    else 
-              let q,r = i lsr 1 , i land 1 in
-              let l = mk_hform t in
-              let l = if r = 0 then l else neg l in
-	      if q = 0 then l
-	      else get reify (Fapp(Fnot2 q, [|l|]))
-	| _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
-	  
-      and mk_fand acc args = 
-	match args with
-	| [t1;t2] -> 
-	    let l2 = mk_hform t2 in
-	    let c, args = Term.decompose_app t1 in
-	    if Term.eq_constr c (Lazy.force candb) then
-              mk_fand (l2::acc) args
-	    else 
-	      let l1 = mk_hform t1 in
-	      get reify (Fapp(Fand, Array.of_list  (l1::l2::acc)))
-	| _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb" 
-
-      and mk_for acc args = 
-	match args with
-	| [t1;t2] -> 
-	    let l2 = mk_hform t2 in
-	    let c, args = Term.decompose_app t1 in
-	    if Term.eq_constr c (Lazy.force corb) then
-              mk_for (l2::acc) args
-	    else 
-	      let l1 = mk_hform t1 in
-	      get reify (Fapp(For, Array.of_list (l1::l2::acc)))
-	| _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
-
-      let l = mk_hform c in
-      l
+        match args with
+        | [t] ->
+           let c,args = Term.decompose_app t in
+           if Term.eq_constr c (Lazy.force cnegb) then
+             mk_fnot (i+1) args
+           else
+             let q,r = i lsr 1 , i land 1 in
+             let l = mk_hform t in
+             let l = if r = 0 then l else neg l in
+             if q = 0 then l
+             else get reify (Fapp(Fnot2 q, [|l|]))
+        | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
+
+      and mk_fand acc args =
+        match args with
+        | [t1;t2] ->
+           let l2 = mk_hform t2 in
+           let c, args = Term.decompose_app t1 in
+           if Term.eq_constr c (Lazy.force candb) then
+             mk_fand (l2::acc) args
+           else
+             let l1 = mk_hform t1 in
+             get reify (Fapp(Fand, Array.of_list (l1::l2::acc)))
+        | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb"
+
+      and mk_for acc args =
+        match args with
+        | [t1;t2] ->
+           let l2 = mk_hform t2 in
+           let c, args = Term.decompose_app t1 in
+           if Term.eq_constr c (Lazy.force corb) then
+             mk_for (l2::acc) args
+           else
+             let l1 = mk_hform t1 in
+             get reify (Fapp(For, Array.of_list (l1::l2::acc)))
+        | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
+
+      mk_hform c
 
     (** Flattening of Fand and For, removing of Fnot2 *)
     let set_sign f f' =
       if is_pos f then f' else neg f'
 
-    let rec flatten reify f = 
+    let rec flatten reify f =
       match pform f with
       | Fatom _ -> f
       | Fapp(Fnot2 _,args) -> set_sign f (flatten reify args.(0))
       | Fapp(Fand, args) -> set_sign f (flatten_and reify [] (Array.to_list args))
       | Fapp(For,args) -> set_sign f (flatten_or reify [] (Array.to_list args))
       | Fapp(op,args) ->
-          (* TODO change Fimp into For ? *)
-	  set_sign f (get reify (Fapp(op, Array.map (flatten reify) args)))
+         (* TODO change Fimp into For ? *)
+	 set_sign f (get reify (Fapp(op, Array.map (flatten reify) args)))
 
     and flatten_and reify acc args =
       match args with
       | [] -> get reify (Fapp(Fand, Array.of_list (List.rev acc)))
       | a::args ->
-	  (* TODO change (not For) and (not Fimp) into Fand *)
-	  match pform a with
-	  | Fapp(Fand, args') when is_pos a ->
-	      let args = Array.fold_right (fun a args -> a::args) args' args in
-	      flatten_and reify acc args
-	  | _ -> flatten_and reify (flatten reify a :: acc) args
+	 (* TODO change (not For) and (not Fimp) into Fand *)
+	 match pform a with
+	 | Fapp(Fand, args') when is_pos a ->
+	    let args = Array.fold_right (fun a args -> a::args) args' args in
+	    flatten_and reify acc args
+	 | _ -> flatten_and reify (flatten reify a :: acc) args
 
     and flatten_or reify acc args =
       (* TODO change Fimp and (not Fand) into For *)
       match args with
       | [] -> get reify (Fapp(For, Array.of_list (List.rev acc)))
       | a::args ->
-	  match pform a with
-	  | Fapp(For, args') when is_pos a ->
-	      let args = Array.fold_right (fun a args -> a::args) args' args in
-	      flatten_or reify acc args
-	  | _ -> flatten_or reify (flatten reify a :: acc) args
+	 match pform a with
+	 | Fapp(For, args') when is_pos a ->
+	    let args = Array.fold_right (fun a args -> a::args) args' args in
+	    flatten_or reify acc args
+	 | _ -> flatten_or reify (flatten reify a :: acc) args
 
-    (** Producing Coq terms *) 
+    (** Producing Coq terms *)
 
     let to_coq hf = mkInt (to_lit hf)
 
@@ -422,20 +420,20 @@ module Make (Atom:ATOM) =
       let cargs = Array.make (Array.length args + 1) (mkInt 0) in
       Array.iteri (fun i hf -> cargs.(i) <- to_coq hf) args;
       Structures.mkArray (Lazy.force cint, cargs)
-	
+
     let pf_to_coq = function
-      | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|]	
+      | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|]
       | Fapp(op,args) ->
-        match op with
-	| Ftrue -> Lazy.force cFtrue
-	| Ffalse -> Lazy.force cFfalse
-	| Fand -> mklApp cFand [| args_to_coq args|]
-	| For  -> mklApp cFor [| args_to_coq args|]
-	| Fimp -> mklApp cFimp [| args_to_coq args|]
-	| Fxor -> mklApp cFxor (Array.map to_coq args)
-	| Fiff -> mklApp cFiff (Array.map to_coq args)
-	| Fite -> mklApp cFite (Array.map to_coq args)
-	| Fnot2 i -> mklApp cFnot2 [|mkInt i; to_coq args.(0)|]
+         match op with
+	 | Ftrue -> Lazy.force cFtrue
+	 | Ffalse -> Lazy.force cFfalse
+	 | Fand -> mklApp cFand [| args_to_coq args|]
+	 | For  -> mklApp cFor [| args_to_coq args|]
+	 | Fimp -> mklApp cFimp [| args_to_coq args|]
+	 | Fxor -> mklApp cFxor (Array.map to_coq args)
+	 | Fiff -> mklApp cFiff (Array.map to_coq args)
+	 | Fite -> mklApp cFite (Array.map to_coq args)
+	 | Fnot2 i -> mklApp cFnot2 [|mkInt i; to_coq args.(0)|]
 
     let pform_tbl reify =
       let t = Array.make reify.count pform_true in
@@ -464,55 +462,49 @@ module Make (Atom:ATOM) =
     (** [interp_atom] map [Atom.t] to coq term, it is better if it produce
 	shared terms. *)
     let interp_to_coq interp_atom form_tbl f =
-      let rec interp_form f = 
+      let rec interp_form f =
 	let l = to_lit f in
-	try Hashtbl.find form_tbl l 
+	try Hashtbl.find form_tbl l
 	with Not_found ->
-	  if is_neg f then 
-	    let pc = interp_form (neg f) in
-	    let nc = mklApp cnegb [|pc|] in
-	    Hashtbl.add form_tbl l nc;
-	    nc
-	  else
-	    let pc = 
-	      match pform f with
-	      | Fatom a -> interp_atom a
-	      | Fapp(op, args) ->
-		  match op with
-		  | Ftrue -> Lazy.force ctrue
-		  | Ffalse -> Lazy.force cfalse
-		  | Fand -> interp_args candb args
-		  | For -> interp_args corb args
-		  | Fxor -> interp_args cxorb args
-		  | Fimp -> 
-		      let r = ref (interp_form args.(Array.length args - 1)) in
-		      for i = Array.length args - 2 downto 0 do
-			r := mklApp cimplb [|interp_form args.(i); !r|]
-		      done;
-		      !r
-		  | Fiff -> interp_args ceqb args
-		  | Fite -> 
-		      (* TODO with if here *)
-		      mklApp cifb (Array.map interp_form args)
-		  | Fnot2 n -> 
-		      let r = ref (interp_form args.(0)) in
-		      for i = 1 to n do	r := mklApp cnegb [|!r|] done;
-		      !r in 
-	    Hashtbl.add form_tbl l pc;
-	    pc
+	      if is_neg f then
+	        let pc = interp_form (neg f) in
+	        let nc = mklApp cnegb [|pc|] in
+	        Hashtbl.add form_tbl l nc;
+	        nc
+	      else
+	        let pc =
+	          match pform f with
+	          | Fatom a -> interp_atom a
+	          | Fapp(op, args) ->
+		     match op with
+		     | Ftrue -> Lazy.force ctrue
+		     | Ffalse -> Lazy.force cfalse
+		     | Fand -> interp_args candb args
+		     | For -> interp_args corb args
+		     | Fxor -> interp_args cxorb args
+		     | Fimp ->
+		        let r = ref (interp_form args.(Array.length args - 1)) in
+		        for i = Array.length args - 2 downto 0 do
+		          r := mklApp cimplb [|interp_form args.(i); !r|]
+		        done;
+		        !r
+		     | Fiff -> interp_args ceqb args
+		     | Fite ->
+		        (* TODO with if here *)
+		        mklApp cifb (Array.map interp_form args)
+		     | Fnot2 n ->
+		        let r = ref (interp_form args.(0)) in
+		        for i = 1 to n do
+                          r := mklApp cnegb [|!r|]
+                        done;
+                        !r in
+	        Hashtbl.add form_tbl l pc;
+	        pc
       and interp_args op args =
 	let r = ref (interp_form args.(0)) in
-	for i = 1 to Array.length args - 1 do
-	  r := mklApp op [|!r;interp_form args.(i)|] 
-	done;
-	!r in
-      interp_form f
-
-  end
-	
-
-	  
-
-    
-
-  
+	  for i = 1 to Array.length args - 1 do
+	    r := mklApp op [|!r;interp_form args.(i)|]
+	  done;
+	  !r in
+        interp_form f
+end
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index 2a00228..c372bf5 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -37,7 +37,6 @@ type fop =
   | Fiff
   | Fite
   | Fnot2 of int
-
  
 type ('a,'f) gen_pform = 
   | Fatom of 'a
@@ -73,7 +72,7 @@ module type FORM =
       
       (** Given a coq term, build the corresponding formula *)  
       val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
-   
+
       (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
       val flatten : reify -> t -> t
 
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index 4815a77..96d5f0f 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -20,7 +20,7 @@ open SmtCertif
 
 let notUsed = 0
 
-let next_id = ref 0 
+let next_id = ref 0
 
 let clear () = next_id := 0
 
@@ -31,7 +31,7 @@ let next_id () =
 
 (** Basic functions over small certificates *)
 
-let mk_scertif kind ov = 
+let mk_scertif kind ov =
   {
    id   = next_id ();
    kind = kind;
@@ -39,13 +39,13 @@ let mk_scertif kind ov =
    used = notUsed;
    prev = None;
    next = None;
-   value = ov 
+   value = ov
  }
-  
+
 (** Roots *)
 
 
-let mkRootGen ov = 
+let mkRootGen ov =
   let pos = next_id () in
   {
    id   = pos;
@@ -54,17 +54,17 @@ let mkRootGen ov =
    used = notUsed;
    prev = None;
    next = None;
-   value = ov 
+   value = ov
  }
 
 (* let mkRoot = mkRootGen None *)
 let mkRootV v = mkRootGen (Some v)
- 
-let isRoot k = k == Root 
+
+let isRoot k = k == Root
 
 (** Resolutions *)
 
-let mkRes c1 c2 tl = 
+let mkRes c1 c2 tl =
   mk_scertif (Res { rc1 = c1; rc2 = c2; rtail = tl }) None
 
 let isRes k =
@@ -141,7 +141,7 @@ let rec get_pos c =
       | Some n -> n
       | _ -> assert false
       end
-  | Same c -> get_pos c 
+  | Same c -> get_pos c
 
 let eq_clause c1 c2 = (repr c1).id = (repr c2).id
 
@@ -154,49 +154,46 @@ let select c =
   while not (isRoot !r.kind) do
     let p = prev !r in
     (match !r.kind with
-      | Res res ->
-      if !r.used == 1 then begin
-        !r.used <- notUsed;
-        (* let res = get_res !r "select" in *)
-        mark res.rc1; mark res.rc2;
-        List.iter mark res.rtail
-      end else
-        skip !r;
-      | Same _ ->
+     | Res res ->
+        if !r.used == 1 then begin
+            !r.used <- notUsed;
+            (* let res = get_res !r "select" in *)
+            mark res.rc1; mark res.rc2;
+            List.iter mark res.rtail
+          end else
+          skip !r;
+     | Same _ ->
         skip !r
-      | _ ->
-      if !r.used == 1 then 
-	begin
-          !r.used <- notUsed;
-          let rl = get_other !r "select" in
-          List.iter mark (used_clauses rl)
-	end 
-      else skip !r;
+     | _ ->
+        if !r.used == 1 then
+	  begin
+            !r.used <- notUsed;
+            let rl = get_other !r "select" in
+            List.iter mark (used_clauses rl)
+	  end
+        else skip !r;
     );
     r := p
   done
 
- 
 
 
 (* Compute the number of occurence of each_clause *)
-
 let rec occur c =
   match c.kind with
   | Root -> c.used <- c.used + 1
   | Res res ->
-      if c.used == notUsed then 
+      if c.used == notUsed then
 	begin occur res.rc1; occur res.rc2; List.iter occur res.rtail end;
       c.used <- c.used + 1
   | Other res ->
-      if c.used == notUsed then List.iter occur (used_clauses res);
-      c.used <- c.used + 1;
+     if c.used == notUsed then List.iter occur (used_clauses res);
+     c.used <- c.used + 1;
   | Same c' ->
     occur c';
     c.used <- c.used + 1
 
-(* Allocate clause *)
-
+(* Allocate clauses *)
 let alloc c =
   let free_pos = ref [] in
 
@@ -211,12 +208,12 @@ let alloc c =
   done;
 
   (* r is the first clause defined by resolution or another rule,
-     normaly the first used *)
+     normally the first used *)
   let last_set = ref (get_pos (prev !r)) in
 
   let decr_clause c =
     let rc = repr c in
-      assert (rc.used > notUsed);
+    assert (rc.used > notUsed);
     rc.used <- rc.used - 1;
     if rc.used = notUsed then
       free_pos := get_pos rc :: !free_pos in
@@ -231,14 +228,14 @@ let alloc c =
 
   while !r.next <> None do
     let n = next !r in
-      assert (!r.used <> notUsed);
+    assert (!r.used <> notUsed);
     if isRes !r.kind then
       decr_res (get_res !r "alloc")
     else
       decr_other (get_other !r "alloc");
     begin match !free_pos with
-    | p::free -> free_pos := free; !r.pos <- Some p
-    | _ -> incr last_set; !r.pos <- Some !last_set
+          | p::free -> free_pos := free; !r.pos <- Some p
+          | _ -> incr last_set; !r.pos <- Some !last_set
     end;
     r := n
   done;
@@ -277,8 +274,8 @@ let build_certif first_root confl =
 let to_coq to_lit interp (cstep,
     cRes, cImmFlatten,
     cTrue, cFalse, cBuildDef, cBuildDef2, cBuildProj,
-    cImmBuildProj,cImmBuildDef,cImmBuildDef2,  
-    cEqTr, cEqCgr, cEqCgrP, 
+    cImmBuildProj,cImmBuildDef,cImmBuildDef2,
+    cEqTr, cEqCgr, cEqCgrP,
     cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim,
     cHole) confl =
 
@@ -288,7 +285,7 @@ let to_coq to_lit interp (cstep,
   let out_c c = mkInt (get_pos c) in
   let step_to_coq c =
     match c.kind with
-    | Res res -> 
+    | Res res ->
 	let size = List.length res.rtail + 3 in
 	let args = Array.make size (mkInt 0) in
 	args.(0) <- mkInt (get_pos res.rc1);
@@ -296,10 +293,10 @@ let to_coq to_lit interp (cstep,
 	let l = ref res.rtail in
 	for i = 2 to size - 2 do
 	  match !l with
-	  | c::tl -> 
+	  | c::tl ->
 	      args.(i) <- mkInt (get_pos c);
 	      l := tl
-	  | _ -> assert false 
+	  | _ -> assert false
 	done;
 	mklApp cRes [|mkInt (get_pos c); Structures.mkArray (Lazy.force cint, args)|]
     | Other other ->
@@ -346,7 +343,7 @@ let to_coq to_lit interp (cstep,
 	end
     | _ -> assert false in
   let step = Lazy.force cstep in
-  let def_step = 
+  let def_step =
     mklApp cRes [|mkInt 0; Structures.mkArray (Lazy.force cint, [|mkInt 0|]) |] in
   let r = ref confl in
   let nc = ref 0 in
@@ -382,13 +379,13 @@ let to_coq to_lit interp (cstep,
 
 (** Optimization of the trace *)
 
-module MakeOpt (Form:SmtForm.FORM) = 
-  struct 
+module MakeOpt (Form:SmtForm.FORM) =
+  struct
     (* Share the certificate building a common clause *)
     let share_value c =
       let tbl = Hashtbl.create 17 in
       let to_lits v = List.map (Form.to_lit) v in
-      let process c = 
+      let process c =
 	match c.value with
 	| None -> ()
 	| Some v ->
@@ -401,7 +398,7 @@ module MakeOpt (Form:SmtForm.FORM) =
       while !r.next <> None do
 	let next = next !r in
 	process !r;
-	r := next 
+	r := next
       done;
       process !r
 
@@ -430,7 +427,7 @@ module MakeOpt (Form:SmtForm.FORM) =
 	    if eq_clause c1 c2 then aux (repr c1 :: rhd) tl1' tl2'
 	    else List.rev rhd, tl1, tl2
       in aux [] tl1 tl2
-	
+
     let share_prefix first_c n =
       let tbl = HRtbl.create (min n Sys.max_array_length) in
       let rec share c2 =