diff options
Diffstat (limited to 'src/verit/veritSyntax.ml')
| -rw-r--r-- | src/verit/veritSyntax.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |