aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/sos_lib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/sos_lib.ml')
-rw-r--r--plugins/micromega/sos_lib.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index e592611ac..41cbeda3f 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 =