From e12110637730d067c216abcc86185b761189b342 Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Fri, 28 May 2021 18:29:37 +0200
Subject: getting rid of native-coq (#95)

---
 src/smtlib2/smtlib2_genConstr.ml | 8 ++++----
 src/smtlib2/smtlib2_solver.ml    | 6 +++---
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'src/smtlib2')

diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index eb1c5b7..0c6e2ac 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -97,10 +97,10 @@ let rec sort_of_sort = function
 
 
 let declare_sort_from_name rt s =
-  let cons_t = Structures.declare_new_type (Structures.mkId ("Smt_sort_"^s)) in
+  let cons_t = CoqInterface.declare_new_type (CoqInterface.mkId ("Smt_sort_"^s)) in
   let compdec_type = mklApp cCompDec [| cons_t |] in
   let compdec_var =
-    Structures.declare_new_variable (Structures.mkId ("CompDec_"^s)) compdec_type in
+    CoqInterface.declare_new_variable (CoqInterface.mkId ("CompDec_"^s)) compdec_type in
   let res = SmtBtype.of_coq_compdec rt cons_t compdec_var in
   SmtMaps.add_btype s res;
   res
@@ -110,9 +110,9 @@ let declare_sort rt sym = declare_sort_from_name rt (string_of_symbol sym)
 
 let declare_fun_from_name rt ro s tyl ty =
   let coqTy = List.fold_right (fun typ c ->
-      Structures.mkArrow (interp_to_coq rt typ) c)
+      CoqInterface.mkArrow (interp_to_coq rt typ) c)
       tyl (interp_to_coq rt ty) in
-  let cons_v = Structures.declare_new_variable (Structures.mkId ("Smt_var_"^s)) coqTy in
+  let cons_v = CoqInterface.declare_new_variable (CoqInterface.mkId ("Smt_var_"^s)) coqTy in
   let op = Op.declare ro cons_v (Array.of_list tyl) ty None in
   SmtMaps.add_fun s op;
   op
diff --git a/src/smtlib2/smtlib2_solver.ml b/src/smtlib2/smtlib2_solver.ml
index 99538ce..efab1c1 100644
--- a/src/smtlib2/smtlib2_solver.ml
+++ b/src/smtlib2/smtlib2_solver.ml
@@ -73,7 +73,7 @@ let read_response { lexbuf } =
 
 let error s sexp =
   kill s;
-  Structures.error (asprintf "Solver error: %a." SExpr.print sexp)
+  CoqInterface.error (asprintf "Solver error: %a." SExpr.print sexp)
 
 
 let read_success s = 
@@ -89,7 +89,7 @@ let read_check_result s =
   match SExprParser.sexp SExprLexer.main s.lexbuf with
   | SExpr.Atom "sat" -> Sat
   | SExpr.Atom "unsat" -> Unsat
-  | SExpr.Atom "unknown" -> Structures.error ("Solver returned uknown.")
+  | SExpr.Atom "unknown" -> CoqInterface.error ("Solver returned uknown.")
   | r -> error s r
 
 
@@ -111,7 +111,7 @@ let send_command s cmd read =
      *   let buf = Bytes.create err_p2 in
      *   Unix.read s.stderr buf 0 err_p2 |> ignore;
      *   let err_msg = Bytes.sub_string buf err_p1 len in
-     *   Structures.error ("Solver error: "^err_msg);
+     *   CoqInterface.error ("Solver error: "^err_msg);
      * end
      * else (kill s; raise e) *)
     kill s; raise e
-- 
cgit