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/verit/verit.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'src/verit/verit.ml')

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 =
-- 
cgit