diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-07-05 18:22:53 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-05 18:29:00 +0200 |
| commit | b2dd4dd979577e4f384750872f7f0e7f9bd8df94 (patch) | |
| tree | 613c86859810558ec7127a47fc6469ec207b7ca5 /plugins/micromega/sos_types.mli | |
| parent | 82ed3089485ebe0b722d8505ddbd89d73570b8f9 (diff) | |
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.
Diffstat (limited to 'plugins/micromega/sos_types.mli')
| -rw-r--r-- | plugins/micromega/sos_types.mli | 40 |
1 files changed, 0 insertions, 40 deletions
diff --git a/plugins/micromega/sos_types.mli b/plugins/micromega/sos_types.mli deleted file mode 100644 index 57c4e50ca..000000000 --- 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 |