aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-06 10:08:51 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-06 10:08:51 +0000
commit0256a92eb0d0265750bd38a85dce4f9487aefe5b (patch)
treee2786cc2476aebafa664db64da2ab787f18a887a /plugins/micromega
parent30cf9c6711df3eb583dacad3cb98158adbbf1f5f (diff)
still some more dead code removal
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
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 e416c514c..f848591cc 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 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 =