From b2dd4dd979577e4f384750872f7f0e7f9bd8df94 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 5 Jul 2016 18:22:53 +0200
Subject: Revert "Merge remote-tracking branch 'github/pr/229' into trunk"

This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing
changes made to da99355b4d6de31aec5a660f7afe100190a8e683.

Hugo asked for more discussion on this topic, and it was not in the roadmap. I
merged it prematurely because I thought there was a consensus. Also, I missed
that it was changing coq_makefile. Sorry about that.
---
 plugins/micromega/sos_types.mli | 40 ----------------------------------------
 1 file changed, 40 deletions(-)
 delete mode 100644 plugins/micromega/sos_types.mli

(limited to 'plugins')

diff --git a/plugins/micromega/sos_types.mli b/plugins/micromega/sos_types.mli
deleted file mode 100644
index 57c4e50cad..0000000000
--- a/plugins/micromega/sos_types.mli
+++ /dev/null
@@ -1,40 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* The type of positivstellensatz -- used to communicate with sos *)
-
-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);;
-
-val output_term : out_channel -> term -> unit
-
-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;;
-
-val output_psatz : out_channel -> positivstellensatz -> unit
-- 
cgit v1.2.3