2 files changed, 42 insertions, 47 deletions

diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 32f76f1..2fd7d2d 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -10,55 +10,50 @@
 (**************************************************************************)
 
 
-open Entries
-open Declare
-open Decl_kinds
-
 open SmtMisc
 open CoqTerms
-open SmtForm
 open SmtTrace
 open SmtAtom
 open SmtBtype
 open SmtCertif
 
 
-let debug = false
+(* let debug = false *)
 
 
 (******************************************************************************)
 (* Given a verit trace build the corresponding certif and theorem             *)
 (******************************************************************************)
-exception Import_trace of int
+(* exception Import_trace of int *)
 
-let get_val = function
-    Some a -> a
-  | None -> assert false
+(* let get_val = function
+ *     Some a -> a
+ *   | None -> assert false *)
 
 (* For debugging certif processing : <add_scertif> <select> <occur> <alloc> *)
-let print_certif c where=
-  let r = ref c in
-  let out_channel = open_out where in
-  let fmt = Format.formatter_of_out_channel out_channel in
-  let continue = ref true in
-  while !continue do
-    let kind = to_string (!r.kind) in
-    let id = !r.id in
-    let pos = match !r.pos with
-      | None -> "None"
-      | Some p -> string_of_int p in
-    let used = !r.used in
-    Format.fprintf fmt "id:%i kind:%s pos:%s used:%i value:" id kind pos used;
-    begin match !r.value with
-    | None -> Format.fprintf fmt "None"
-    | Some l -> List.iter (fun f -> Form.to_smt Atom.to_smt fmt f;
-                                    Format.fprintf fmt " ") l end;
-    Format.fprintf fmt "\n";
-    match !r.next with
-    | None -> continue := false
-    | Some n -> r := n
-  done;
-  Format.fprintf fmt "@."; close_out out_channel
+(* let print_certif c where=
+ *   let r = ref c in
+ *   let out_channel = open_out where in
+ *   let fmt = Format.formatter_of_out_channel out_channel in
+ *   let continue = ref true in
+ *   while !continue do
+ *     let kind = to_string (!r.kind) in
+ *     let id = !r.id in
+ *     let pos = match !r.pos with
+ *       | None -> "None"
+ *       | Some p -> string_of_int p in
+ *     let used = !r.used in
+ *     Format.fprintf fmt "id:%i kind:%s pos:%s used:%i value:" id kind pos used;
+ *     begin match !r.value with
+ *     | None -> Format.fprintf fmt "None"
+ *     | Some l -> List.iter (fun f -> Form.to_smt Atom.to_smt fmt f;
+ *                                     Format.fprintf fmt " ") l end;
+ *     Format.fprintf fmt "\n";
+ *     match !r.next with
+ *     | None -> continue := false
+ *     | Some n -> r := n
+ *   done;
+ *   Format.fprintf fmt "@."; close_out out_channel *)
 
 let import_trace ra' rf' filename first lsmt =
   let chan = open_in filename in
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index e209fd2..6b26f65 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -193,18 +193,18 @@ let mkDistinctElim old value =
 
 (* Clause difference (wrt to their sets of literals) *)
 
-let clause_diff c1 c2 =
-  let r =
-    List.filter (fun t1 -> not (List.exists (SmtAtom.Form.equal t1) c2)) c1
-  in
-  Format.eprintf "[";
-  List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c1;
-  Format.eprintf "] -- [";
-  List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c2;
-  Format.eprintf "] ==\n [";
-  List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) r;
-  Format.eprintf "] @.";
-  r
+(* let clause_diff c1 c2 =
+ *   let r =
+ *     List.filter (fun t1 -> not (List.exists (SmtAtom.Form.equal t1) c2)) c1
+ *   in
+ *   Format.eprintf "[";
+ *   List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c1;
+ *   Format.eprintf "] -- [";
+ *   List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c2;
+ *   Format.eprintf "] ==\n [";
+ *   List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) r;
+ *   Format.eprintf "] @.";
+ *   r *)
 
 
 
@@ -234,7 +234,7 @@ let rec fins_lemma ids_params =
                 Other (Forall_inst (lemma, _)) -> lemma
               | _ -> fins_lemma t
 
-let rec find_remove_lemma lemma ids_params =
+let find_remove_lemma lemma ids_params =
   let eq_lemma h = eq_clause lemma (get_clause h) in
   list_find_remove eq_lemma ids_params
 
@@ -250,7 +250,7 @@ let rec merge ids_params =
 
 let to_add = ref []
 
-let rec mk_clause (id,typ,value,ids_params) =
+let mk_clause (id,typ,value,ids_params) =
   let kind =
     match typ with
       (* Roots *)