getting rid of native-coq (#95)

3 files changed, 16 insertions, 16 deletions

diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index eed1dca..7f89943 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -193,25 +193,25 @@ let call_verit _ rt ro ra_quant rf_quant first lsmt =
         if l = "warning : proof_done: status is still open" then
           raise Unknown
         else if l = "Invalid memory reference" then
-          Structures.warning "verit-warning" ("veriT outputted the warning: " ^ l)
+          CoqInterface.warning "verit-warning" ("veriT outputted the warning: " ^ l)
         else if n >= 7 && String.sub l 0 7 = "warning" then
-          Structures.warning "verit-warning" ("veriT outputted the warning: " ^ (String.sub l 7 (n-7)))
+          CoqInterface.warning "verit-warning" ("veriT outputted the warning: " ^ (String.sub l 7 (n-7)))
         else if n >= 8 && String.sub l 0 8 = "error : " then
-          Structures.error ("veriT failed with the error: " ^ (String.sub l 8 (n-8)))
+          CoqInterface.error ("veriT failed with the error: " ^ (String.sub l 8 (n-8)))
         else
-          Structures.error ("veriT failed with the error: " ^ l)
+          CoqInterface.error ("veriT failed with the error: " ^ l)
       done
     with End_of_file -> () in
 
   try
-    if exit_code <> 0 then Structures.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code);
+    if exit_code <> 0 then CoqInterface.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code);
     raise_warnings_errors ();
     let res = import_trace ra_quant rf_quant logfilename (Some first) lsmt in
     close_in win; Sys.remove wname; res
   with x -> close_in win; Sys.remove wname;
             match x with
-            | Unknown -> Structures.error "veriT returns 'unknown'"
-            | VeritSyntax.Sat -> Structures.error "veriT found a counter-example"
+            | Unknown -> CoqInterface.error "veriT returns 'unknown'"
+            | VeritSyntax.Sat -> CoqInterface.error "veriT found a counter-example"
             | _ -> raise x
 
 let verit_logic =
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 0560d77..f0acd0c 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -11,13 +11,13 @@
 
 
 val parse_certif :
-  Structures.id ->
-  Structures.id ->
-  Structures.id ->
-  Structures.id ->
-  Structures.id -> Structures.id -> Structures.id -> string -> string -> unit
+  CoqInterface.id ->
+  CoqInterface.id ->
+  CoqInterface.id ->
+  CoqInterface.id ->
+  CoqInterface.id -> CoqInterface.id -> CoqInterface.id -> string -> string -> unit
 val checker : string -> string -> unit
 val checker_debug : string -> string -> unit
-val theorem : Structures.id -> string -> string -> unit
-val tactic : EConstr.t -> Structures.constr_expr list -> Structures.tactic
-val tactic_no_check : EConstr.t -> Structures.constr_expr list -> Structures.tactic
+val theorem : CoqInterface.id -> string -> string -> unit
+val tactic : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
+val tactic_no_check : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index 21c10e8..c5db594 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -493,7 +493,7 @@ let mk_clause (id,typ,value,ids_params) =
 let mk_clause cl =
   try mk_clause cl
   with Failure f ->
-    Structures.error ("SMTCoq was not able to check the certificate \
+    CoqInterface.error ("SMTCoq was not able to check the certificate \
                        for the following reason.\n"^f)
 
 let apply_dec f (decl, a) = decl, f a