aboutsummaryrefslogtreecommitdiffstats
path: root/src/lfsc/tosmtcoq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/lfsc/tosmtcoq.ml')
-rw-r--r--src/lfsc/tosmtcoq.ml8
1 files changed, 3 insertions, 5 deletions
diff --git a/src/lfsc/tosmtcoq.ml b/src/lfsc/tosmtcoq.ml
index 0395244..f520ba7 100644
--- a/src/lfsc/tosmtcoq.ml
+++ b/src/lfsc/tosmtcoq.ml
@@ -12,8 +12,6 @@
open SmtAtom
open SmtForm
-open SmtCertif
-open SmtTrace
open VeritSyntax
open Ast
open Builtin
@@ -42,7 +40,7 @@ module HT = struct
let add h k v = h := M.add k v !h
let find h k = M.find k !h
let clear h = h := M.empty
- let iter f h = M.iter f !h
+ (* let iter f h = M.iter f !h *)
end
@@ -499,8 +497,8 @@ let register_clause_id cl id =
Hashtbl.add ids_clauses id cl
-let register_termclause_id t id =
- register_clause_id (to_clause t) id
+(* let register_termclause_id t id =
+ * register_clause_id (to_clause t) id *)
let new_clause_id ?(reuse=true) cl =