aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/csdpcert.ml3
-rw-r--r--plugins/micromega/sos_lib.ml4
2 files changed, 3 insertions, 4 deletions
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index e416c514c9..f848591cc9 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -12,7 +12,6 @@
(* *)
(************************************************************************)
-open Big_int
open Num
open Sos
open Sos_types
@@ -60,7 +59,7 @@ open Mutils
-let rec canonical_sum_to_string = function s -> failwith "not implemented"
+let canonical_sum_to_string = function s -> failwith "not implemented"
let print_canonical_sum m = Format.print_string (canonical_sum_to_string m)
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index e592611acd..41cbeda3f8 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -6,7 +6,7 @@
(* independent bits *)
(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *)
(* ========================================================================= *)
-open Sos_types
+
open Num
let debugging = ref false;;
@@ -546,7 +546,7 @@ let fix err prs input =
try prs input
with Noparse -> failwith (err ^ " expected");;
-let rec listof prs sep err =
+let listof prs sep err =
prs ++ many (sep ++ fix err prs >> snd) >> (fun (h,t) -> h::t);;
let possibly prs input =