From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 plugins/nsatz/ideal.mli | 31 +++++++++++++++++++------------
 1 file changed, 19 insertions(+), 12 deletions(-)

(limited to 'plugins/nsatz/ideal.mli')

diff --git a/plugins/nsatz/ideal.mli b/plugins/nsatz/ideal.mli
index d1a2a0a7..96572808 100644
--- a/plugins/nsatz/ideal.mli
+++ b/plugins/nsatz/ideal.mli
@@ -1,11 +1,24 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+type metadata = {
+  name_var : string list;
+}
+
+module Monomial :
+sig
+type t
+val repr : t -> int array
+val make : int array -> t
+end
+
 module Make (P : Polynom.S) :
 sig
 (* Polynomials *)
@@ -14,32 +27,26 @@ type deg = int
 type coef = P.t
 type poly
 
-val repr : poly -> (coef * int array) list
+val repr : poly -> (coef * Monomial.t) list
 val polconst : int -> coef -> poly
 val zeroP : poly
 val gen : int -> int -> poly
 
 val equal : poly -> poly -> bool
-val name_var : string list ref
 
 val plusP : poly -> poly -> poly
 val oppP : poly -> poly
 val multP : poly -> poly -> poly
 val puisP : poly -> int -> poly
 
-val poldepcontent : coef list ref
-
 type certificate =
     { coef : coef; power : int;
       gb_comb : poly list list; last_comb : poly list }
 
-val in_ideal : deg -> poly list -> poly -> poly list * poly * certificate
+val in_ideal : metadata -> deg -> poly list -> poly -> certificate
 
 module Hashpol : Hashtbl.S with type key = poly
 
-val sugar_flag : bool ref
-val divide_rem_with_critical_pair : bool ref
-
 end
 
 exception NotInIdeal
-- 
cgit v1.2.3