diff options
Diffstat (limited to 'plugins/nsatz/ideal.mli')
| -rw-r--r-- | plugins/nsatz/ideal.mli | 31 |
1 files changed, 19 insertions, 12 deletions
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 |