diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-03-31 20:25:05 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-03-31 20:25:05 +0200 |
| commit | 20831b39a73ebd38336f19ad4ddb4d6b1078d60d (patch) | |
| tree | 9e4ec27753feff8f7e95274f99eaa977b546c030 /src/verit/veritSyntax.ml | |
| parent | 4c8654c57666e27637ba2f60ee5c6455176c7a1d (diff) | |
| download | smtcoq-20831b39a73ebd38336f19ad4ddb4d6b1078d60d.tar.gz smtcoq-20831b39a73ebd38336f19ad4ddb4d6b1078d60d.zip | |
Compiles with Coq-8.10
Diffstat (limited to 'src/verit/veritSyntax.ml')
| -rw-r--r-- | src/verit/veritSyntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml index b1a6304..862a628 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" |