diff options
Diffstat (limited to 'src/verit')
| -rw-r--r-- | src/verit/verit.ml | 14 | ||||
| -rw-r--r-- | src/verit/verit.mli | 16 | ||||
| -rw-r--r-- | src/verit/veritSyntax.ml | 6 |
3 files changed, 18 insertions, 18 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 e0f0fcc..c5db594 100644 --- a/src/verit/veritSyntax.ml +++ b/src/verit/veritSyntax.ml @@ -150,7 +150,7 @@ let mkCongrPred p = (* Linear arithmetic *) let mkMicromega cl = - let _tbl, _f, cert = Lia.build_lia_certif cl in + let cert = Lia.build_lia_certif cl in let c = match cert with | None -> failwith "VeritSyntax.mkMicromega: micromega can't solve this" @@ -168,7 +168,7 @@ let mkSplArith orig cl = match orig.value with | Some [orig'] -> orig' | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the premise clause" in - let _tbl, _f, cert = Lia.build_lia_certif [Form.neg orig';res] in + let cert = Lia.build_lia_certif [Form.neg orig';res] in let c = match cert with | None -> failwith "VeritSyntax.mkSplArith: micromega can't solve this" @@ -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 |