aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/simplex.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2020-03-26 11:25:10 +0100
committerThéo Zimmermann2020-03-26 11:25:10 +0100
commitb398a4eb55c42a97d7d177839d5033a306ee7d52 (patch)
tree707105889c62bdba854398e10c32df9ffdb470e0 /plugins/micromega/simplex.ml
parent63f2da5b3703a16c7722b91ce2f2c78617dec9a7 (diff)
parent7e6b2c6311933f8ef947935f5d4b5897816ab3e4 (diff)
Merge PR #11832: [ocamlformat] Use doc-comments=before style.
Reviewed-by: Zimmi48
Diffstat (limited to 'plugins/micromega/simplex.ml')
-rw-r--r--plugins/micromega/simplex.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index 702099a95d..eaa26ded62 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -62,9 +62,9 @@ let get_profile_info () =
type iset = unit IMap.t
-type tableau = Vect.t IMap.t
(** Mapping basic variables to their equation.
All variables >= than a threshold rst are restricted.*)
+type tableau = Vect.t IMap.t
module Restricted = struct
type t =
@@ -366,9 +366,9 @@ let push_real (opt : bool) (nw : var) (v : Vect.t) (rst : Restricted.t)
let v' = safe_find "push_real" nw t' in
Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.neg_one v'))) )
-open Mutils
(** One complication is that equalities needs some pre-processing.
*)
+open Mutils
open Polynomial