git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 31 deletions

diff --git a/plugins/micromega/sos.mli b/plugins/micromega/sos.mli
index 31c9518c8..42e22ffec 100644
--- a/plugins/micromega/sos.mli
+++ b/plugins/micromega/sos.mli
@@ -6,33 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-
-type vname = string;;
-
-type term =
-| Zero
-| Const of Num.num
-| Var of vname
-| Inv of term
-| Opp of term
-| Add of (term * term)
-| Sub of (term * term)
-| Mul of (term * term)
-| Div of (term * term)
-| Pow of (term * int)
-
-type positivstellensatz =
-   Axiom_eq of int
- | Axiom_le of int
- | Axiom_lt of int
- | Rational_eq of Num.num
- | Rational_le of Num.num
- | Rational_lt of Num.num
- | Square of term
- | Monoid of int list
- | Eqmul of term * positivstellensatz
- | Sum of positivstellensatz * positivstellensatz
- | Product of positivstellensatz * positivstellensatz
+open Sos_types
 
 type poly
 
@@ -55,10 +29,6 @@ val term_of_sos : positivstellensatz * (Num.num * poly) list ->
 
 val string_of_poly : poly -> string
 
-exception TooDeep
-
-val deepen_until : int -> (int -> 'a) -> int -> 'a
-
 val real_positivnullstellensatz_general : bool -> int -> poly list ->
      (poly * positivstellensatz) list ->
      poly -> poly list * (positivstellensatz * (Num.num * poly) list) list