aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/simplex.mli
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-12-13 15:41:53 +0100
committerEmilio Jesus Gallego Arias2019-12-13 21:27:08 +0100
commit8b8a3858f34782eeb489c43c758e8c8c1f75c108 (patch)
treee8589934668b1475d1a562f00cd3e646845f307d /plugins/micromega/simplex.mli
parentc8cc1ac7fabb52ddfe50aee714bb7e1a1c3d3bc1 (diff)
[micromega] Enable ocamlformat.
Diffstat (limited to 'plugins/micromega/simplex.mli')
-rw-r--r--plugins/micromega/simplex.mli5
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/micromega/simplex.mli b/plugins/micromega/simplex.mli
index cba8e94ea7..19bcce3590 100644
--- a/plugins/micromega/simplex.mli
+++ b/plugins/micromega/simplex.mli
@@ -10,9 +10,8 @@
open Polynomial
val optimise : Vect.t -> cstr list -> (Num.num option * Num.num option) option
-
val find_point : cstr list -> Vect.t option
-
val find_unsat_certificate : cstr list -> Vect.t option
-val integer_solver : (cstr * ProofFormat.prf_rule) list -> ProofFormat.proof option
+val integer_solver :
+ (cstr * ProofFormat.prf_rule) list -> ProofFormat.proof option