aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/sos.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/sos.mli')
-rw-r--r--plugins/micromega/sos.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/sos.mli b/plugins/micromega/sos.mli
index 42e22ffec..e38caba06 100644
--- a/plugins/micromega/sos.mli
+++ b/plugins/micromega/sos.mli
@@ -24,7 +24,7 @@ val poly_of_term : term -> poly
val term_of_poly : poly -> term
-val term_of_sos : positivstellensatz * (Num.num * poly) list ->
+val term_of_sos : positivstellensatz * (Num.num * poly) list ->
positivstellensatz
val string_of_poly : poly -> string