Adding support for lemmas in the command verit

18 files changed, 570 insertions, 211 deletions

diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 1874d5f..96d5a69 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -90,6 +90,8 @@ let csigT = gen_constant init_modules "sigT"
 let cnot = gen_constant init_modules "not"
 let ceq = gen_constant init_modules "eq"
 let crefl_equal = gen_constant init_modules "eq_refl"
+let cconj = gen_constant init_modules "conj"
+let cand = gen_constant init_modules "and"
 
 (* SMT_terms *)
 
@@ -179,7 +181,7 @@ let make_certif_ops modules args =
   gen_constant"ImmBuildDef2",
   gen_constant "EqTr", gen_constant "EqCgr", gen_constant "EqCgrP", 
   gen_constant "LiaMicromega", gen_constant "LiaDiseq", gen_constant "SplArith", gen_constant "SplDistinctElim",
-  gen_constant "Hole")
+  gen_constant "Hole", gen_constant "ForallInst")
   
 
 (** Useful construction *)
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index 8fd166e..7d7fe6a 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -45,6 +45,8 @@ val csigT : Term.constr lazy_t
 val cnot : Term.constr lazy_t
 val ceq : Term.constr lazy_t
 val crefl_equal : Term.constr lazy_t
+val cconj : Term.constr lazy_t
+val cand : Term.constr lazy_t
 val smt_modules : string list list
 val cState_C_t : Term.constr lazy_t
 val cdistinct : Term.constr lazy_t
@@ -106,7 +108,7 @@ val make_certif_ops :
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-  Term.constr lazy_t
+  Term.constr lazy_t * Term.constr lazy_t 
 val ceq_refl_true : Term.constr lazy_t
 val eq_refl_true : unit -> Term.constr
 val vm_cast_true : Term.constr -> Term.constr
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
index 5d4201b..4577d42 100644
--- a/src/trace/satAtom.mli
+++ b/src/trace/satAtom.mli
@@ -28,14 +28,15 @@ module Form :
     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
+    val to_string : ?pi:bool -> (hatom -> string) -> t -> string
+    val to_smt : (hatom -> string) -> Format.formatter -> t -> unit
     exception NotWellTyped of pform
     type reify = SmtForm.Make(Atom).reify
     val create : unit -> reify
     val clear : reify -> unit
-    val get : reify -> pform -> t
+    val get : ?declare:bool -> reify -> pform -> t
     val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+    val hash_hform : (hatom -> hatom) -> reify -> t -> t
     val flatten : reify -> t -> t
     val to_coq : t -> Term.constr
     val pform_tbl : reify -> pform array
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index ed0402c..7ccaa95 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -49,17 +49,18 @@ type op_def = {
     tres : btype;
     op_val : Term.constr }
 
-type indexed_op = op_def gen_hashed 
+type index = Index of int
+           | Rel_name of string
 
-let dummy_indexed_op i dom codom = {index = i; hval = {tparams = dom; tres = codom; op_val = Term.mkProp}}
-let indexed_op_index op = op.index
+type indexed_op = index * op_def
 
-type op = 
-  | Cop of cop
-  | Uop of uop
-  | Bop of bop
-  | Nop of nop
-  | Iop of indexed_op
+let destruct s (i, hval) = match i with
+  | Index index -> index, hval
+  | Rel_name _ -> failwith s
+
+let dummy_indexed_op i dom codom = i, {tparams = dom; tres = codom; op_val = Term.mkProp}
+let indexed_op_index i = let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in
+                         index
 
 module Op =
   struct
@@ -159,11 +160,12 @@ module Op =
     let interp_nop = function
       | NO_distinct ty -> mklApp cdistinct [|interp_distinct ty;interp_eq ty|]
 
-    let i_to_coq i = mkInt i.index
+    let i_to_coq i = let index, _ = destruct "destruct on a Rel: called by i_to_coq" i in
+                     mkInt index
 
-    let i_type_of i = i.hval.tres
+    let i_type_of (_, hval) = hval.tres
 
-    let i_type_args i = i.hval.tparams
+    let i_type_args (_, hval) = hval.tparams
 
     (* reify table *)
     type reify_tbl =
@@ -175,13 +177,15 @@ module Op =
       { count = 0;
 	tbl =  Hashtbl.create 17 }
 
-    let declare reify op tparams tres =
+    let declare reify op tparams tres os =
       assert (not (Hashtbl.mem reify.tbl op));
-      let v = { tparams = tparams; tres = tres; op_val = op } in
-      let res = {index = reify.count; hval = v } in
-      Hashtbl.add reify.tbl op res;
-      reify.count <- reify.count + 1;
-      res
+      let opa = { tparams = tparams; tres = tres; op_val = op } in
+      match os with
+      | None ->  let res = Index reify.count, opa in
+                 Hashtbl.add reify.tbl op res;
+                 reify.count <- reify.count + 1;
+                 res
+      | Some name -> Rel_name name, opa
 
     let of_coq reify op =
       Hashtbl.find reify.tbl op
@@ -190,15 +194,16 @@ 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 set _ op =
+        let index, hval = destruct "destruct on a Rel: called by set in interp_tbl" op in
+        t.(index) <- mk_Tval hval.tparams hval.tres hval.op_val in
       Hashtbl.iter set reify.tbl;
       Structures.mkArray (tval, t)
 
     let to_list reify =
       let set _ op acc =
-        let value = op.hval in
-        (op.index,value.tparams,value.tres,op)::acc in
+        let index, hval = destruct "destruct on a Rel: called by set in to_list" op in
+        (index, hval.tparams, hval.tres, op)::acc in
       Hashtbl.fold set reify.tbl []
 
     let c_equal op1 op2 = op1 == op2
@@ -214,7 +219,7 @@ module Op =
       match op1,op2 with
       | NO_distinct t1, NO_distinct t2 -> SmtBtype.equal t1 t2
 
-    let i_equal op1 op2 = op1.index == op2.index
+    let i_equal (i1, _) (i2, _) = i1 = i2
 
   end
 
@@ -294,13 +299,14 @@ module HashedAtom =
            | _ -> 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 op_index = try fst (destruct "destruct on a Rel: called by hash" op) with _ -> 0 in
          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
+         (hash_args lsl 5 + op_index lsl 3) lxor 4
 
   end
 
@@ -343,33 +349,44 @@ module Atom =
 
     and compute_hint h = compute_int (atom h)
 
-    let to_smt_int fmt i =
+    let to_string_int i =
       let s1 = if i < 0 then "(- " else "" in
       let s2 = if i < 0 then ")" else "" in
       let j = if i < 0 then -i else i in
-      Format.fprintf fmt "%s%i%s" s1 j s2
-
-    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;
-            Format.fprintf fmt ")"
-          )
-
-      and to_smt_bop fmt op h1 h2 =
+      s1 ^ string_of_int j ^ s2
+
+    let to_string ?pi:(pi=false) h =
+      let rec to_string h = 
+        (if pi then string_of_int (index h) ^":" else "")
+        ^ to_string_atom (atom h)
+
+      and to_string_atom = function
+        | Acop _ as a -> to_string_int (compute_int a)
+        | Auop (UO_Zopp,h) -> 
+           "(- " ^
+             to_string h ^
+               ")"
+        | Auop _ as a -> to_string_int (compute_int a)
+        | Abop (op,h1,h2) -> to_string_bop op h1 h2
+        | Anop (op,a) -> to_string_nop op a
+        | Aapp ((i, op), a) ->
+           let op_string = begin match i with
+                           | Index index -> "op_" ^ string_of_int index
+                           | Rel_name name -> name end
+                           ^ if pi then to_string_op op else "" in
+           if Array.length a = 0 then (
+             op_string
+           ) else (
+             "(" ^ op_string ^
+               Array.fold_left (fun acc h -> acc ^ " " ^ to_string h) "" a ^
+                 ")"
+           )
+      and to_string_op {tparams=bta; tres=bt; op_val=t} =
+        "[(" ^ Array.fold_left (fun acc bt -> acc ^ SmtBtype.to_string bt ^ " ")
+                 " " bta ^ ") ( " ^ SmtBtype.to_string bt ^ " ) ( " ^
+          Pp.string_of_ppcmds (Printer.pr_constr t) ^ " )]"
+
+      and to_string_bop op h1 h2 =
         let s = match op with
           | BO_Zplus -> "+"
           | BO_Zminus -> "-"
@@ -379,19 +396,21 @@ module Atom =
           | 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 ")"
+        "(" ^ s ^ " " ^
+          to_string h1 ^
+            " " ^
+              to_string h2 ^
+                ")"
 
-      and to_smt_nop fmt op a =
+      and to_string_nop 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 ")"
+        "(" ^ s ^
+          Array.fold_left (fun acc h -> acc ^ " " ^ to_string h) "" a ^
+            ")" in
+      to_string h
 
+    let to_smt fmt t = Format.fprintf fmt "%s@." (to_string t)
 
 
     exception NotWellTyped of atom
@@ -436,9 +455,58 @@ module Atom =
       reify.count <- reify.count + 1;
       res
 
-    let get reify a =
-      try HashAtom.find reify.tbl a
-      with Not_found -> declare reify a
+    let get ?declare:(decl=true) reify a =
+      if decl
+      then try HashAtom.find reify.tbl a
+           with Not_found -> declare reify a
+      else {index = -1; hval = a}
+
+    let mk_eq reify decl ty h1 h2 =
+      let op = BO_eq ty in
+      try
+        HashAtom.find reify.tbl (Abop (op, h1, h2))
+      with Not_found ->
+        try
+          HashAtom.find reify.tbl (Abop (op, h2, h1))
+        with Not_found ->
+          get ~declare:decl reify (Abop (op, h1, h2))
+
+    let mk_neg reify ({index = i; hval = a} as ha) =
+      try HashAtom.find reify.tbl (Auop (UO_Zopp, ha))
+      with Not_found -> 
+        let na = match a with
+          | Auop (UO_Zpos, x) -> Auop (UO_Zneg, x)
+          | Auop (UO_Zneg, x) -> Auop (UO_Zpos, x)
+          | _ -> failwith "opp not on Z" in
+        get reify na
+
+    let rec hash_hatom ra' {index = _; hval = a} =
+      match a with 
+      | Acop cop -> get ra' a
+      | Auop (uop, ha) -> get ra' (Auop (uop, hash_hatom ra' ha))
+      | Abop (bop, ha1, ha2) ->
+         let new_ha1 = hash_hatom ra' ha1 in
+         let new_ha2 = hash_hatom ra' ha2 in
+         begin match bop with
+         | BO_eq ty -> mk_eq ra' true ty new_ha1 new_ha2
+         | _ -> get ra' (Abop (bop, new_ha1, new_ha2)) end
+      | Anop _ -> assert false
+      | Aapp (op, arr) -> get ra' (Aapp (op, Array.map (hash_hatom ra') arr))
+              
+    let copy {count=c; tbl=t} = {count = c; tbl = HashAtom.copy t}
+             
+    let print_atoms reify where =
+      let oc = open_out where in
+      let fmt = Format.formatter_of_out_channel oc in
+      let accumulate _ ha acc = ha :: acc in
+      let list = HashAtom.fold accumulate reify.tbl [] in
+      let compare ha1 ha2 = compare ha1.index ha2.index in
+      let slist = List.sort compare list in
+      let print ha = Format.fprintf fmt "%i: " ha.index;
+                     to_smt fmt ha; Format.fprintf fmt "\n" in
+      List.iter print slist;
+      Format.fprintf fmt "@.";
+      close_out oc
 
 
     (** Given a coq term, build the corresponding atom *)
@@ -476,11 +544,10 @@ module Atom =
 
     let op_tbl = lazy (op_tbl ())
 
-    let of_coq rt ro reify env sigma c =
+    let of_coq ?hash:(h=false) rt ro reify env sigma c =
       let op_tbl = Lazy.force op_tbl in
       let get_cst c =
 	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
 	match get_cst c with
@@ -498,21 +565,32 @@ module Atom =
         | 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)
+        | CCeqb -> mk_teq Tbool args
+        | CCeqbP -> mk_teq Tpositive args
+        | CCeqbZ -> mk_teq TZ args
+	| CCunknown -> let ty = Retyping.get_type_of env sigma h in
+                       mk_unknown c args ty
+
+      and mk_cop op = get reify (Acop op)
 
       and mk_uop op = function
         | [a] -> let h = mk_hatom a in get reify (Auop (op,h))
-        | _ -> assert false
+        | _ -> failwith "unexpected number of arguments for mk_uop"
+
+      and mk_teq ty args = 
+        if h then match args with    
+        | [a1; a2] -> let h1 = mk_hatom a1 in
+                      let h2 = mk_hatom a2 in
+                      mk_eq reify true ty h1 h2
+        | _ -> failwith "unexpected number of arguments for mk_teq"
+        else mk_bop (BO_eq ty) args
 
       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))
-        | _ -> assert false
+        | _ -> failwith "unexpected number of arguments for mk_bop"
 
       and mk_unknown c args ty =
         let hargs = Array.of_list (List.map mk_hatom args) in
@@ -520,7 +598,12 @@ module Atom =
                  with Not_found ->
                    let targs = Array.map type_of hargs in
                    let tres = SmtBtype.of_coq rt ty in
-                   Op.declare ro c targs tres in
+                   let os = if Term.isRel c
+                            then let i = Term.destRel c in
+                                 let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in
+                                 Some (string_of_name n)
+                            else None in
+                   Op.declare ro c targs tres os in
         get reify (Aapp (op,hargs)) in
 
       mk_hatom c
@@ -572,7 +655,7 @@ module Atom =
                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
+            | Aapp ((_, hval),t) -> Term.mkApp (hval.op_val, Array.map interp_atom t) in
 	  Hashtbl.add atom_tbl l pc;
 	  pc in
       interp_atom a
@@ -580,11 +663,11 @@ module Atom =
 
     (* Generation of atoms *)
 
-    let mk_nop op reify a = get reify (Anop (op,a))
+    let mk_nop op reify ?declare:(decl=true) a = get ~declare:decl reify (Anop (op,a))
 
-    let mk_binop op reify h1 h2 = get reify (Abop (op, h1, h2))
+    let mk_binop op reify decl h1 h2 = get ~declare:decl reify (Abop (op, h1, h2))
 
-    let mk_unop op reify h = get reify (Auop (op, h))
+    let mk_unop op reify ?declare:(decl=true) h = get ~declare:decl reify (Auop (op, h))
 
     let rec hatom_pos_of_int reify i =
       if i <= 1 then
@@ -621,17 +704,7 @@ module Atom =
         else
           mk_unop UO_Zneg reify (hatom_pos_of_bigint reify (Big_int.minus_big_int i))
 
-    let mk_eq reify ty h1 h2 =
-      let op = BO_eq ty in
-      try
-        HashAtom.find reify.tbl (Abop (op, h1, h2))
-      with
-        | Not_found ->
-          try
-            HashAtom.find reify.tbl (Abop (op, h2, h1))
-          with
-            | Not_found ->
-              declare reify (Abop (op, h1, h2))
+    let mk_unop op reify ?declare:(decl=true) h = get ~declare:decl reify (Auop (op, h))
 
     let mk_lt = mk_binop BO_Zlt
     let mk_le = mk_binop BO_Zle
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index 8e69265..47734fb 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -43,7 +43,10 @@ type nop =
 
 type indexed_op
 
-val dummy_indexed_op: int -> btype array -> btype -> indexed_op
+type index = Index of int
+           | Rel_name of string
+
+val dummy_indexed_op: index -> btype array -> btype -> indexed_op
 val indexed_op_index : indexed_op -> int
 
 module Op :
@@ -53,7 +56,8 @@ module Op :
 
     val create : unit -> reify_tbl
 
-    val declare : reify_tbl -> Term.constr -> btype array -> btype -> indexed_op
+    val declare : reify_tbl -> Term.constr -> btype array ->
+                  btype -> string option -> indexed_op
 
     val of_coq : reify_tbl -> Term.constr -> indexed_op
 
@@ -92,6 +96,8 @@ module Atom :
  
       val type_of : hatom -> btype
 
+      val to_string : ?pi:bool -> hatom -> string
+                               
       val to_smt : Format.formatter -> t -> unit
 
       exception NotWellTyped of atom
@@ -102,10 +108,22 @@ module Atom :
 
       val clear : reify_tbl -> unit
 
-      val get : reify_tbl -> atom -> hatom
+      val get : ?declare:bool -> reify_tbl -> atom -> hatom
+
+      val mk_eq : reify_tbl -> bool -> btype -> hatom -> hatom -> hatom
+
+      val mk_neg : reify_tbl -> hatom -> hatom
+                                                                    
+      val hash_hatom : reify_tbl -> hatom -> hatom
+
+      (** for debugging purposes **)
 
+      val copy : reify_tbl -> reify_tbl
+                                                        
+      val print_atoms : reify_tbl -> string -> unit
+                                       
       (** Given a coq term, build the corresponding atom *)
-      val of_coq : SmtBtype.reify_tbl -> Op.reify_tbl ->
+      val of_coq : ?hash:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
         reify_tbl -> Environ.env -> Evd.evar_map -> Term.constr -> t
 
       val to_coq : hatom -> Term.constr
@@ -121,16 +139,15 @@ module Atom :
       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
-      val mk_gt : reify_tbl -> hatom -> hatom -> hatom
-      val mk_ge : reify_tbl -> hatom -> hatom -> hatom
-      val mk_plus : reify_tbl -> hatom -> hatom -> hatom
-      val mk_minus : reify_tbl -> hatom -> hatom -> hatom
-      val mk_mult : reify_tbl -> hatom -> hatom -> hatom
-      val mk_opp : reify_tbl -> hatom -> hatom
-      val mk_distinct : reify_tbl -> btype -> hatom array -> hatom
+      val mk_lt : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_le : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_gt : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_ge : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_plus : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_minus : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_mult : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_opp : reify_tbl -> ?declare:bool -> hatom -> hatom
+      val mk_distinct : reify_tbl -> btype -> ?declare:bool -> hatom array -> hatom
 
     end
 
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index 92b8ad7..f3245ea 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -18,13 +18,15 @@ type btype =
 let index_tbl = Hashtbl.create 17
 
 let index_to_coq i =
-  let i = i.index in 
   try Hashtbl.find index_tbl i
   with Not_found ->
     let interp = mklApp cTindex [|mkInt i|] in
     Hashtbl.add index_tbl i interp;
     interp
 
+let indexed_type_of_int i =
+  {index = i; hval = index_to_coq i }
+      
 let equal t1 t2 =
   match t1,t2 with
   | Tindex i, Tindex j -> i.index == j.index
@@ -34,13 +36,15 @@ let to_coq = function
   | TZ -> Lazy.force cTZ
   | Tbool -> Lazy.force cTbool
   | Tpositive -> Lazy.force cTpositive
-  | Tindex i -> index_to_coq i
+  | Tindex i -> index_to_coq i.index
 
-let to_smt fmt = function
-  | TZ -> Format.fprintf fmt "Int"
-  | Tbool -> Format.fprintf fmt "Bool"
-  | Tpositive -> Format.fprintf fmt "Int"
-  | Tindex i -> Format.fprintf fmt "Tindex_%i" i.index
+let to_string = function
+  | TZ -> "Int"
+  | Tbool -> "Bool"
+  | Tpositive -> "Int"
+  | Tindex i -> "Tindex_" ^ string_of_int i.index
+
+let to_smt fmt b = Format.fprintf fmt "%s" (to_string b)
 
 (* reify table *)
 type reify_tbl =
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli
index 11d596f..29e91bf 100644
--- a/src/trace/smtBtype.mli
+++ b/src/trace/smtBtype.mli
@@ -3,14 +3,16 @@ val dummy_indexed_type : int -> indexed_type
 val indexed_type_index : indexed_type -> int
 val indexed_type_hval : indexed_type -> Term.constr
 type btype = TZ | Tbool | Tpositive | Tindex of indexed_type
+val indexed_type_of_int : int -> indexed_type
 val equal : btype -> btype -> bool
 val to_coq : btype -> Term.constr
+val to_string : btype -> string
 val to_smt : Format.formatter -> btype -> unit
 type reify_tbl
 val create : unit -> reify_tbl
+val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list
 val declare : reify_tbl -> Term.constr -> Term.constr -> btype
-val of_coq : reify_tbl -> Term.constr -> btype
+val of_coq : reify_tbl -> Term.types -> btype
 val interp_tbl : reify_tbl -> Term.constr
 val to_list : reify_tbl -> (int * indexed_type) list
-val interp_to_coq : reify_tbl -> btype -> Term.constr
-val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list
+val interp_to_coq : 'a -> btype -> Term.constr
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index a0972d4..a0af59d 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -110,15 +110,17 @@ type 'hform rule =
 
   (* Possibility to introduce "holes" in proofs (that should be filled in Coq) *)
   | Hole of ('hform clause) list * 'hform list
+  | Forall_inst of 'hform clause * 'hform
+  | Qf_lemma of 'hform clause * 'hform
 
 and 'hform clause = {
-            id    : clause_id;
+    mutable 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
+    mutable value : 'hform list option
               (* This field should be defined for rules which can create atoms :
                  EqTr, EqCgr, EqCgrP, Lia, Dlde, Lra *)
 }
@@ -137,8 +139,45 @@ and 'hform resolution = {
 let used_clauses r =
   match r with
   | ImmBuildProj (c, _) | ImmBuildDef c | ImmBuildDef2 c
-  | ImmFlatten (c,_)  | SplArith (c,_,_) | SplDistinctElim (c,_) -> [c]
+  | ImmFlatten (c,_)  | SplArith (c,_,_) | SplDistinctElim (c,_)
+  | Forall_inst (c, _) | Qf_lemma (c, _) -> [c]
   | Hole (cs, _) -> cs
   | True | False | BuildDef _ | BuildDef2 _ | BuildProj _
   | EqTr _ | EqCgr _ | EqCgrP _
   | LiaMicromega _ | LiaDiseq _ -> []
+
+(* for debugging *)                                       
+let to_string r =
+  match r with
+            Root -> "Root"
+          | Same c -> "Same(" ^ string_of_int (c.id) ^ ")"
+          | Res r ->
+             let id1 = string_of_int r.rc1.id in
+             let id2 = string_of_int r.rc2.id in
+             let rest_ids = List.fold_left (fun str rc -> str ^ "; " ^ string_of_int rc.id) "" r.rtail in
+             "Res [" ^ id1 ^ "; " ^ id2 ^ rest_ids ^"]"
+          | Other x -> "Other(" ^
+                         begin match x with
+                         | True -> "True"
+                         | False -> "False"
+                         | BuildDef _ -> "BuildDef"
+                         | BuildDef2 _ -> "BuildDef2"
+                         | BuildProj _ -> "BuildProj"
+                         | EqTr _ -> "EqTr"
+                         | EqCgr _ -> "EqCgr"
+                         | EqCgrP _ -> "EqCgrP"
+                         | LiaMicromega _ -> "LiaMicromega"
+                         | LiaDiseq _ -> "LiaDiseq"
+                         | Qf_lemma _ -> "Qf_lemma"
+                                         
+                         | Hole _ -> "Hole"
+
+                         | ImmFlatten _ -> "ImmFlatten"
+                         | ImmBuildDef _ -> "ImmBuildDef"
+                         | ImmBuildDef2 _ -> "ImmBuildDef2"
+                         | ImmBuildProj _ -> "ImmBuildProj"
+                         | SplArith _ -> "SplArith"
+                         | SplDistinctElim _ -> "SplDistinctElim"
+                         | Forall_inst _ -> "Forall_inst"  end ^ ")"
+
+
diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli
index 767dc8b..942262c 100644
--- a/src/trace/smtCertif.mli
+++ b/src/trace/smtCertif.mli
@@ -20,15 +20,17 @@ type 'hform rule =
       Structures.Micromega_plugin_Certificate.Mc.zArithProof list
   | SplDistinctElim of 'hform clause * 'hform
   | Hole of 'hform clause list * 'hform list
+  | Forall_inst of 'hform clause * 'hform
+  | Qf_lemma of 'hform clause * 'hform
 
 and 'hform clause = {
-            id    : clause_id;
+    mutable 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;
+    mutable value : 'hform list option;
 }
 and 'hform clause_kind =
     Root
@@ -41,3 +43,4 @@ and 'hform resolution = {
   mutable rtail : 'hform clause list;
 }
 val used_clauses : 'a rule -> 'a clause list
+val to_string : 'a clause_kind -> string
diff --git a/src/trace/smtCnf.ml b/src/trace/smtCnf.ml
index bf3d0d1..62a040d 100644
--- a/src/trace/smtCnf.ml
+++ b/src/trace/smtCnf.ml
@@ -149,7 +149,8 @@ module MakeCnf (Form:FORM) =
 		  cnf c
 
 	      | Fnot2 _ -> cnf args.(0)
- 
+              | Fforall _ -> assert false
+
     exception Cnf_done
 
     let rec imm_link_Other other l =
@@ -245,6 +246,7 @@ module MakeCnf (Form:FORM) =
 		  push_cnf args
 
               | Fnot2 _ -> assert false
+              | Fforall _ -> assert false
 
     let make_cnf reify c =
       let ftrue = Form.get reify (Fapp(Ftrue, [||])) in
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index ba86a5b..27b8210 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -38,6 +38,7 @@ let cchecker_b = gen_constant euf_checker_modules "checker_b"
 let cchecker_eq_correct =
   gen_constant euf_checker_modules "checker_eq_correct"
 let cchecker_eq = gen_constant euf_checker_modules "checker_eq"
+let cZeqbsym = gen_constant z_modules "eqb_sym"
 
 (* Given an SMT-LIB2 file and a certif, build the corresponding objects *)
 
@@ -105,7 +106,8 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
   let ce2 = Structures.mkUConst t_form' in
   let ct_form = Term.mkConst (declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition)) in
 
-  let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl in
+  (* EMPTY LEMMA LIST *)
+  let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
   List.iter (fun (v,ty) ->
     let _ = Structures.declare_new_variable v ty in
     print_assm ty
@@ -160,7 +162,8 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
 
-  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl in
+  (* EMPTY LEMMA LIST *)
+  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
   List.iter (fun (v,ty) ->
     let _ = Structures.declare_new_variable v ty in
     print_assm ty
@@ -182,7 +185,7 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
     List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
     Structures.mkArray (Lazy.force cint, res) in
 
-  let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots roots|]|] in
+  let theorem_concl = mklApp cis_true [|mklApp cnegb [|interp_roots roots|]|] in
   let theorem_proof_cast =
     Term.mkCast (
         Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
@@ -234,7 +237,8 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
 
-  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl in
+  (* EMPTY LEMMA LIST *)
+  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
   List.iter (fun (v,ty) ->
     let _ = Structures.declare_new_variable v ty in
     print_assm ty
@@ -274,7 +278,7 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
 
 (* Tactic *)
 
-let build_body rt ro ra rf l b (max_id, confl) =
+let build_body rt ro ra rf l b (max_id, confl) find =
   let nti = mkName "t_i" in
   let ntfunc = mkName "t_func" in
   let ntatom = mkName "t_atom" in
@@ -287,7 +291,7 @@ let build_body rt ro ra rf l b (max_id, confl) =
   let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
-  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl in
+  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl find in
   let certif =
     mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
 
@@ -314,7 +318,7 @@ let build_body rt ro ra rf l b (max_id, confl) =
   (proof_cast, proof_nocast, cuts)
 
 
-let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) =
+let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) find =
   let nti = mkName "t_i" in
   let ntfunc = mkName "t_func" in
   let ntatom = mkName "t_atom" in
@@ -327,7 +331,7 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) =
   let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i*))) in
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
-  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl in
+  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl find in
   let certif =
     mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
 
@@ -362,26 +366,89 @@ let get_arguments concl =
   | _ -> failwith ("Verit.tactic: can only deal with equality over bool")
 
 
-let make_proof call_solver rt ro rf l =
-  let fl = Form.flatten rf l in
-  let root = SmtTrace.mkRootV [l] in
-  call_solver rt ro fl (root,l)
-
-
-let core_tactic call_solver rt ro ra rf env sigma concl =
+let make_proof call_solver rt ro rf ra' rf' l' ls_smtc=
+  let fl' = Form.flatten rf' l' in
+  let root = SmtTrace.mkRootV [l'] in
+  call_solver rt ro ra' rf' (Some (root, l')) (fl'::ls_smtc)
+
+(* <of_coq_lemma> reifies the coq lemma given, we can then easily print it in a
+ .smt2 file. We need the reify tables to correctly recognize unbound variables
+ of the lemma. We also need to make sure to leave unchanged the tables because
+ the new objects may contain bound (by forall of the lemma) variables. *)
+exception Axiom_form_unsupported
+              
+let of_coq_lemma rt ro ra' rf' env sigma clemma =
+  let rel_context, qf_lemma = Term.decompose_prod_assum clemma in
+  let env_lemma = List.fold_right Environ.push_rel rel_context env in
+  let forall_args =
+    let fmap r = let n, t = Structures.destruct_rel_decl r in
+                 string_of_name n, SmtBtype.of_coq rt t in
+    List.map fmap rel_context in
+  let f, args = Term.decompose_app qf_lemma in
+  let core_f =
+    if Term.eq_constr f (Lazy.force cis_true) then
+      match args with
+      | [a] -> a
+      | _ -> raise Axiom_form_unsupported
+    else if Term.eq_constr f (Lazy.force ceq) then
+      match args with
+      | [ty; arg1; arg2] when Term.eq_constr ty (Lazy.force cbool) &&
+                                Term.eq_constr arg2 (Lazy.force ctrue) ->
+         arg1
+      | _ -> raise Axiom_form_unsupported
+    else raise Axiom_form_unsupported in
+  let core_smt = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env_lemma sigma)
+                   rf' core_f in
+  match forall_args with
+    [] -> core_smt
+  | _ -> Form.get rf' (Fapp (Fforall forall_args, [|core_smt|]))
+
+let core_tactic call_solver rt ro ra rf ra' rf' lcpl lcepl env sigma concl =
   let a, b = get_arguments concl in
+  let tlcepl = List.map (Structures.interp_constr env sigma) lcepl in
+  let lcpl = lcpl @ tlcepl in
+  let lcl = List.map (Retyping.get_type_of env sigma) lcpl in
+
+  let lsmt  = List.map (of_coq_lemma rt ro ra' rf' env sigma) lcl in
+  let l_pl_ls = List.combine (List.combine lcl lcpl) lsmt in
+
+  let lem_tbl : (int, Term.constr * Term.constr) Hashtbl.t =
+    Hashtbl.create 100 in
+  let new_ref ((l, pl), ls) =
+    Hashtbl.add lem_tbl (Form.index ls) (l, pl) in
+
+  List.iter new_ref l_pl_ls;
+  
+  let find_lemma cl =
+    let re_hash hf = Form.hash_hform (Atom.hash_hatom ra') rf' hf in
+    match cl.value with
+    | Some [l] ->
+       let hl = re_hash l in
+       begin try Hashtbl.find lem_tbl (Form.index hl)
+             with Not_found ->
+               let oc = open_out "/tmp/find_lemma.log" in
+               List.iter (fun u -> Printf.fprintf oc "%s\n"
+                                     (VeritSyntax.string_hform u)) lsmt;
+               Printf.fprintf oc "\n%s\n" (VeritSyntax.string_hform hl);
+               flush oc; close_out oc; failwith "find_lemma" end
+      | _ -> failwith "unexpected form of root" in
+  
   let (body_cast, body_nocast, cuts) =
     if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then
       let l = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
-      let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
-      let max_id_confl = make_proof call_solver rt ro rf l' in
-      build_body rt ro ra rf (Form.to_coq l) b max_id_confl
+      let l' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env sigma) rf' a in
+      let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l' else l' in
+      let max_id_confl = make_proof call_solver rt ro rf ra' rf' l' lsmt in
+      build_body rt ro ra rf (Form.to_coq l) b max_id_confl (Some find_lemma)
     else
       let l1 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
       let l2 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf b in
       let l = Form.neg (Form.get rf (Fapp(Fiff,[|l1;l2|]))) in
-      let max_id_confl = make_proof call_solver rt ro rf l in
-      build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl in
+      let l1' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env sigma) rf' a in
+      let l2' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env sigma) rf' b in
+      let l' = Form.neg (Form.get rf' (Fapp(Fiff,[|l1';l2'|]))) in
+      let max_id_confl = make_proof call_solver rt ro rf ra' rf' l' lsmt in
+      build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl (Some find_lemma) in
 
   let cuts = SmtBtype.get_cuts rt @ cuts in
 
@@ -392,7 +459,7 @@ let core_tactic call_solver rt ro ra rf env sigma concl =
        (Structures.set_evars_tac body_nocast)
        (Structures.vm_cast_no_check body_cast))
 
-let tactic call_solver rt ro ra rf =
+let tactic call_solver rt ro ra rf ra' rf' lcpl lcepl =
   Structures.tclTHEN
     Tactics.intros
-    (Structures.mk_tactic (core_tactic call_solver rt ro ra rf))
+    (Structures.mk_tactic (core_tactic call_solver rt ro ra rf ra' rf' lcpl lcepl))
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
index 3cac245..6248270 100644
--- a/src/trace/smtCommands.mli
+++ b/src/trace/smtCommands.mli
@@ -7,7 +7,7 @@ val certif_ops :
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
   Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
-  Term.constr lazy_t
+  Term.constr lazy_t * Term.constr lazy_t
 val cCertif : Term.constr lazy_t
 val ccertif : Term.constr lazy_t
 val cchecker : Term.constr lazy_t
@@ -53,6 +53,7 @@ val build_body :
   Term.constr ->
   Term.constr ->
   int * SmtAtom.Form.t SmtCertif.clause ->
+  (SmtAtom.Form.t SmtCertif.clause  -> Term.constr * Term.constr) option ->
   Term.constr * Term.constr * (Names.identifier * Term.types) list
 val build_body_eq :
   SmtBtype.reify_tbl ->
@@ -63,30 +64,35 @@ val build_body_eq :
   Term.constr ->
   Term.constr ->
   int * SmtAtom.Form.t SmtCertif.clause ->
+  (SmtAtom.Form.t SmtCertif.clause  -> Term.constr * Term.constr) option ->
   Term.constr * Term.constr * (Names.identifier * Term.types) list
 val get_arguments : Term.constr -> Term.constr * Term.constr
 val make_proof :
-  ('a ->
-   'b ->
-   SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> 'c) ->
-  'a -> 'b -> SmtAtom.Form.reify -> SmtAtom.Form.t -> 'c
-val core_tactic :
-  (SmtBtype.reify_tbl ->
-   SmtAtom.Op.reify_tbl ->
-   SmtAtom.Form.t ->
-   SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
-   int * SmtAtom.Form.t SmtCertif.clause) ->
-  SmtBtype.reify_tbl ->
-  SmtAtom.Op.reify_tbl ->
-  SmtAtom.Atom.reify_tbl ->
+  (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
+   SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+   (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
+   SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause) ->
+  SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
   SmtAtom.Form.reify ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+  SmtAtom.Form.t -> SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause
+val core_tactic :
+  (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
+   SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+   (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
+   SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause) ->
+  SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+  Term.constr list -> Structures.constr_expr list -> 
   Environ.env -> Evd.evar_map -> Term.constr -> Structures.tactic
 val tactic :
-  (SmtBtype.reify_tbl ->
-   SmtAtom.Op.reify_tbl ->
-   SmtAtom.Form.t ->
-   SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
-   int * SmtAtom.Form.t SmtCertif.clause) ->
+  (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
+   SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+   (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
+   SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause) ->
   SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
-  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Structures.tactic
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
+  Term.constr list -> Structures.constr_expr list -> Structures.tactic
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 069f2ec..c408343 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -17,6 +17,7 @@
 open Util
 open SmtMisc
 open CoqTerms
+open SmtBtype
 
 module type ATOM =
   sig
@@ -41,6 +42,7 @@ type fop =
   | Fiff
   | Fite
   | Fnot2 of int
+  | Fforall of (string * btype) list
 
 type ('a,'f) gen_pform =
   | Fatom of 'a
@@ -66,18 +68,21 @@ module type FORM =
     val is_pos : t -> bool
     val is_neg : t -> bool
 
-      val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
+    val to_string : ?pi:bool -> (hatom -> string) -> t -> string
+    val to_smt : (hatom -> string) -> 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
+    val get : ?declare:bool -> reify -> pform -> t
 
     (** Give a coq term, build the corresponding formula *)
     val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
 
+    val hash_hform : (hatom -> hatom) -> reify -> t -> t
     (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
     val flatten : reify -> t -> t
 
@@ -145,20 +150,22 @@ module Make (Atom:ATOM) =
       | Pos hp -> hp.hval
       | Neg hp -> hp.hval
 
+    let rec to_string ?pi:(pi=false) atom_to_string = function
+      | Pos hp -> (if pi then string_of_int hp.index ^ ":" else "")
+                  ^ to_string_pform atom_to_string hp.hval
+      | Neg hp -> (if pi then string_of_int hp.index ^ ":" else "") ^ "(not "
+                  ^ to_string_pform atom_to_string hp.hval ^ ")"
 
-    let rec to_smt atom_to_smt fmt = function
-      | Pos hp -> to_smt_pform atom_to_smt fmt hp.hval
-      | Neg hp ->
-        Format.fprintf fmt "(not ";
-        to_smt_pform atom_to_smt fmt hp.hval;
-        Format.fprintf fmt ")"
+    and to_string_pform atom_to_string = function
+      | Fatom a -> atom_to_string a
+      | Fapp (op,args) -> to_string_op_args atom_to_string op args
 
-    and to_smt_pform atom_to_smt fmt = function
-      | Fatom a -> atom_to_smt fmt a
-      | Fapp (op,args) -> to_smt_op atom_to_smt fmt op args
+    and to_string_op_args atom_to_string op args =
+      let (s1,s2) = if Array.length args = 0 then ("","") else ("(",")") in
+      s1 ^ to_string_op op ^
+        Array.fold_left (fun acc h -> acc ^ " " ^ to_string atom_to_string h) "" args ^ s2
 
-    and to_smt_op atom_to_smt fmt op args =
-      let s = match op with
+    and to_string_op = function
         | Ftrue -> "true"
         | Ffalse -> "false"
         | Fand -> "and"
@@ -167,12 +174,26 @@ module Make (Atom:ATOM) =
         | Fimp -> "=>"
         | Fiff -> "="
         | Fite -> "ite"
-        | Fnot2 _ -> "" in
-      let (s1,s2) = if Array.length args = 0 then ("","") else ("(",")") in
-      Format.fprintf fmt "%s%s" s1 s;
-      Array.iter (fun h -> Format.fprintf fmt " "; to_smt atom_to_smt fmt h) args;
-      Format.fprintf fmt "%s" s2
-
+        | Fnot2 _ -> ""
+        | Fforall l -> "forall (" ^
+                       to_string_args l ^
+                       ")"
+                                                                                
+    and to_string_args = function
+      | [] -> " "
+      | (s, t)::rest -> " (" ^ s ^ " " ^ SmtBtype.to_string t ^ ")"
+                        ^ to_string_args rest
+
+    let dumbed_down op =
+      let dumbed_down_bt = function
+        | Tindex it -> Tindex (dummy_indexed_type (indexed_type_index it))
+        | x -> x in
+      match op with
+      | Fforall l -> Fforall (List.map (fun (x, bt) -> x, dumbed_down_bt bt) l)
+      | x -> x
+
+    let to_smt atom_to_string fmt f =
+      Format.fprintf fmt "%s" (to_string atom_to_string f)
 
     module HashedForm =
       struct
@@ -182,8 +203,8 @@ module Make (Atom:ATOM) =
 	let equal pf1 pf2 =
 	  match pf1, pf2 with
 	  | Fatom ha1, Fatom ha2 -> Atom.equal ha1 ha2
-	  | Fapp(op1,args1), Fapp(op2,args2) ->
-	      op1 = op2 && 
+	  | Fapp(op1,args1), Fapp(op2,args2) -> 
+	     dumbed_down op1 = dumbed_down op2 && 
 	       Array.length args1 == Array.length args2 &&
 	         (try
 		    for i = 0 to Array.length args1 - 1 do
@@ -205,7 +226,7 @@ module Make (Atom:ATOM) =
 	       | _ ->
 		  (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
+	     (hash_args * 10 + Hashtbl.hash (dumbed_down op)) * 2 + 1
 
       end
 
@@ -232,6 +253,7 @@ module Make (Atom:ATOM) =
 	    if Array.length args <> 2 then raise (NotWellTyped pf)
 	 | Fite ->
 	    if Array.length args <> 3 then raise (NotWellTyped pf)
+         | Fforall l -> ()
 
     let declare reify pf =
       check pf;
@@ -255,9 +277,11 @@ module Make (Atom:ATOM) =
       let _ = declare r pform_false in
       ()
 
-    let get reify pf =
-      try HashForm.find reify.tbl pf
-      with Not_found -> declare reify pf
+    let get ?declare:(decl=true) reify pf =
+      if decl then 
+        try HashForm.find reify.tbl pf
+        with Not_found -> declare reify pf
+      else Pos {index = -1; hval = pf}
 
     (** Given a coq term, build the corresponding formula *)
     type coq_cst =
@@ -376,6 +400,17 @@ module Make (Atom:ATOM) =
 
       mk_hform c
 
+    let hash_hform hash_hatom rf' hf =
+      let rec mk_hform = function
+        | Pos hp -> Pos (mk_hpform hp)
+        | Neg hp -> Neg (mk_hpform hp)
+      and mk_hpform {index = _; hval = hv} =
+        let new_hv = match hv with
+          | Fatom a -> Fatom (hash_hatom a)
+          | Fapp (fop, arr) -> Fapp (fop, Array.map mk_hform arr) in
+        match get rf' new_hv with Pos x | Neg x -> x in
+      mk_hform hf
+
     (** Flattening of Fand and For, removing of Fnot2 *)
     let set_sign f f' =
       if is_pos f then f' else neg f'
@@ -434,6 +469,7 @@ module Make (Atom:ATOM) =
 	 | 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)|]
+         | Fforall _ -> failwith "pf_to_coq on forall"
 
     let pform_tbl reify =
       let t = Array.make reify.count pform_true in
@@ -497,7 +533,8 @@ module Make (Atom:ATOM) =
 		        for i = 1 to n do
                           r := mklApp cnegb [|!r|]
                         done;
-                        !r in
+                        !r
+                     |Fforall _ -> failwith "interp_to_coq on forall" in
 	        Hashtbl.add form_tbl l pc;
 	        pc
       and interp_args op args =
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index c372bf5..4ee86e2 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -37,6 +37,7 @@ type fop =
   | Fiff
   | Fite
   | Fnot2 of int
+  | Fforall of (string * SmtBtype.btype) list 
  
 type ('a,'f) gen_pform = 
   | Fatom of 'a
@@ -61,18 +62,21 @@ module type FORM =
       val is_pos : t -> bool
       val is_neg : t -> bool
 
-      val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
+      val to_string : ?pi:bool -> (hatom -> string) -> t -> string
+      val to_smt : (hatom -> string) -> 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
+      val get : ?declare:bool -> reify -> pform -> t
       
       (** Given a coq term, build the corresponding formula *)  
       val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
 
+      val hash_hform : (hatom -> hatom) -> reify -> t -> t
+                                             
       (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
       val flatten : reify -> t -> t
 
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 1ad92ac..58de402 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -38,3 +38,7 @@ let declare_new_variable = Structures.declare_new_variable
 let mkName s =
   let id = Names.id_of_string s in
   Names.Name id
+
+let string_of_name = function
+    Names.Name id -> Names.string_of_id id
+  | _ -> failwith "unnamed rel"
diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli
index d6aa792..e5cf69f 100644
--- a/src/trace/smtMisc.mli
+++ b/src/trace/smtMisc.mli
@@ -5,3 +5,4 @@ val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr
 val declare_new_type : Names.variable -> Term.constr
 val declare_new_variable : Names.variable -> Term.types -> Term.constr
 val mkName : string -> Names.name
+val string_of_name : Names.name -> string
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index 96d5f0f..9042b8b 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -118,7 +118,9 @@ let get_res c s =
 let get_other c s =
   match c.kind with
   | Other res -> res
-  | _ -> Printf.printf "get_other %s\n" s; assert false
+  | Same _ -> failwith "get_other on a Same"
+  | Res _ -> failwith "get_other on a Res"
+  | Root -> failwith "get_other on a Root"
 
 let get_val c =
   match c.value with
@@ -145,7 +147,86 @@ let rec get_pos c =
 
 let eq_clause c1 c2 = (repr c1).id = (repr c2).id
 
+
+(* Reorders the roots according to the order they were given in initially. *)
+let order_roots init_index first =
+  let r = ref first in
+  let acc = ref [] in
+  while isRoot !r.kind do
+    begin match !r.value with
+    | Some [f] -> let n = next !r in
+                  clear_links !r; 
+                  acc := (init_index f, !r) :: !acc;
+                  r := n
+    | _ -> failwith "root value has unexpected form" end
+  done;
+  let _, lr = List.sort (fun (i1, _) (i2, _) -> Pervasives.compare i1 i2) !acc
+             |> List.split in
+  let link_to c1 c2 =
+    let curr_id = c2.id -1 in
+    c1.id <- curr_id;
+    c1.pos <- Some curr_id;
+    link c1 c2; c1 in
+  List.fold_right link_to lr !r, lr
+
+
+(* <add_scertifs> adds the clauses <to_add> after the roots and makes sure that 
+the following clauses reference those clauses instead of the roots *)
+let add_scertifs to_add c =
+  let r = ref c in
+  clear (); ignore (next_id ());
+  while isRoot !r.kind do
+    ignore (next_id ());
+    r := next !r;
+  done;
+  let after_roots = !r in
+  r := prev !r;
+  let tbl : (int, 'a SmtCertif.clause) Hashtbl.t =
+    Hashtbl.create 17 in
+  let rec push_all = function
+    | [] -> ()
+    | (kind, ov, t_cl)::t -> let cl = mk_scertif kind ov in
+                             Hashtbl.add tbl t_cl.id cl;
+                             link !r cl;
+                             r := next !r;
+                             push_all t in
+  push_all to_add; link !r after_roots; r:= after_roots;
+  let uc c = try Hashtbl.find tbl c.id
+             with Not_found -> c in
+  let update_kind = function
+    | Root -> Root
+    | Same c -> Same (uc c)
+    | Res {rc1 = r1; rc2 = r2; rtail = rt} ->
+       Res {rc1 = uc r1;
+            rc2 = uc r2;
+            rtail = List.map uc rt}
+    | Other u ->
+       Other begin match u with
+         | ImmBuildProj (c, x) -> ImmBuildProj (uc c, x)
+         | ImmBuildDef c -> ImmBuildDef (uc c)
+         | ImmBuildDef2 c -> ImmBuildDef2 (uc c)
+         | Forall_inst (c, x) -> Forall_inst (uc c, x) 
+         | ImmFlatten (c, x) -> ImmFlatten (uc c, x) 
+         | SplArith (c, x, y) -> SplArith (uc c, x, y) 
+         | SplDistinctElim (c, x) -> SplDistinctElim (uc c, x) 
+
+         | Hole (cs, x) -> Hole (List.map uc cs, x)
+
+         | x -> x end in
+  let continue = ref true in
+  while !continue do
+    !r.kind <- update_kind !r.kind;
+    !r.id <- next_id ();
+    match !r.next with 
+    | None -> continue := false
+    | Some n -> r := n
+  done;
+  !r
+
 (* Selection of useful rules *)
+(* For <select>, <occur> and <alloc> we assume that the roots and only the 
+roots are at the beginning of the smtcoq certif *)
+(* After <select> no selected clauses are used so that <occur> works properly*)
 let select c =
   let mark c =
     if not (isRoot c.kind) then c.used <- 1 in
@@ -162,7 +243,8 @@ let select c =
             List.iter mark res.rtail
           end else
           skip !r;
-     | Same _ ->
+     | Same c ->
+        mark c;
         skip !r
      | _ ->
         if !r.used == 1 then
@@ -176,9 +258,8 @@ let select c =
     r := p
   done
 
-
-
-(* Compute the number of occurence of each_clause *)
+(* Compute the number of occurence of each clause so that <alloc> works 
+properly *)
 let rec occur c =
   match c.kind with
   | Root -> c.used <- c.used + 1
@@ -226,23 +307,22 @@ let alloc c =
   let decr_other o =
     List.iter decr_clause (used_clauses o) in
 
-  while !r.next <> None do
-    let n = next !r in
+  let continue = ref true in
+  while !continue do
     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
+    begin try match !free_pos with
+              | p::free -> free_pos := free; !r.pos <- Some p
+              | _ -> incr last_set; !r.pos <- Some !last_set
+          with _ -> failwith (to_string !r.kind)
     end;
-    r := n
+    match !r.next with
+    | None -> continue := false
+    | Some n -> r := n
   done;
-  begin match !free_pos with
-  | p::free -> free_pos := free; !r.pos <- Some p
-  | _ -> incr last_set; !r.pos <- Some !last_set
-  end;
   !last_set
 
 
@@ -277,12 +357,13 @@ let to_coq to_lit interp (cstep,
     cImmBuildProj,cImmBuildDef,cImmBuildDef2,
     cEqTr, cEqCgr, cEqCgrP,
     cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim,
-    cHole) confl =
+    cHole, cForallInst) confl sf =
 
   let cuts = ref [] in
 
   let out_f f = to_lit f in
   let out_c c = mkInt (get_pos c) in
+  let out_cl cl = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in
   let step_to_coq c =
     match c.kind with
     | Res res ->
@@ -335,11 +416,20 @@ let to_coq to_lit interp (cstep,
            let ass_ty = interp (prem, concl) in
            cuts := (ass_name, ass_ty)::!cuts;
            let ass_var = Term.mkVar ass_name in
-           let out_cl cl = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in
            let prem_id' = List.fold_right (fun c l -> mklApp ccons [|Lazy.force cint; out_c c; l|]) prem_id (mklApp cnil [|Lazy.force cint|]) in
            let prem' = List.fold_right (fun cl l -> mklApp ccons [|Lazy.force cState_C_t; out_cl cl; l|]) prem (mklApp cnil [|Lazy.force cState_C_t|]) in
            let concl' = out_cl concl in
            mklApp cHole [|out_c c; prem_id'; prem'; concl'; ass_var|]
+        | Forall_inst (cl, concl) | Qf_lemma (cl, concl) ->
+           let clemma, cplemma = match sf with
+             | Some find -> find cl
+             | None -> assert false in
+           let concl' = out_cl [concl] in
+           let app_name = Names.id_of_string ("app" ^ (string_of_int (Hashtbl.hash concl))) in
+           let app_var = Term.mkVar app_name in
+           let app_ty = Term.mkArrow clemma (interp ([], [concl])) in
+           cuts := (app_name, app_ty)::!cuts;
+           mklApp cForallInst [|out_c c; clemma; cplemma; concl'; app_var|]
 	end
     | _ -> assert false in
   let step = Lazy.force cstep in
@@ -373,7 +463,8 @@ let to_coq to_lit interp (cstep,
   (*   trace.(q) <- Structures.mkArray (step, traceq) *)
   (* end; *)
   (* (Structures.mkArray (mklApp carray [|step|], trace), last_root, !cuts) *)
-  (Structures.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r, last_root, !cuts)
+  let tres = Structures.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r in
+  (tres, last_root, !cuts)
 
 
 
diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli
index 533725b..57d0d42 100644
--- a/src/trace/smtTrace.mli
+++ b/src/trace/smtTrace.mli
@@ -25,6 +25,10 @@ val repr : 'a SmtCertif.clause -> 'a SmtCertif.clause
 val set_same : 'a SmtCertif.clause -> 'a SmtCertif.clause -> unit
 val get_pos : 'a SmtCertif.clause -> int
 val eq_clause : 'a SmtCertif.clause -> 'b SmtCertif.clause -> bool
+val order_roots : ('a -> int) -> 'a SmtCertif.clause ->
+                  'a SmtCertif.clause * 'a SmtCertif.clause list
+val add_scertifs : ('a SmtCertif.clause_kind * 'a list option * 'a SmtCertif.clause) list -> 
+                   'a SmtCertif.clause -> 'a SmtCertif.clause
 val select : 'a SmtCertif.clause -> unit
 val occur : 'a SmtCertif.clause -> unit
 val alloc : 'a SmtCertif.clause -> int
@@ -32,16 +36,16 @@ val naive_alloc : 'a SmtCertif.clause -> int
 val build_certif : 'a SmtCertif.clause -> 'b SmtCertif.clause -> int
 val to_coq :
   ('a -> Term.constr) ->
-  ('a list list * 'a list -> 'b) ->
+  ('a list list * 'a list -> Term.types) ->
   Term.types Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
   Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
   Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
   Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
   Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
   Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
-  Term.constr Lazy.t ->
-  'a SmtCertif.clause ->
-  Term.constr * 'a SmtCertif.clause * (Names.identifier * 'b) list
+  Term.constr Lazy.t * Term.constr Lazy.t -> 'a SmtCertif.clause ->
+  ('a SmtCertif.clause -> Term.constr * Term.constr) option ->
+  Term.constr * 'a SmtCertif.clause * (Names.identifier * Term.types) list
 module MakeOpt :
   functor (Form : SmtForm.FORM) ->
     sig