diff options
Diffstat (limited to 'plugins/nsatz/ideal.mli')
-rw-r--r-- | plugins/nsatz/ideal.mli | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/plugins/nsatz/ideal.mli b/plugins/nsatz/ideal.mli new file mode 100644 index 00000000..d1a2a0a7 --- /dev/null +++ b/plugins/nsatz/ideal.mli @@ -0,0 +1,47 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +module Make (P : Polynom.S) : +sig +(* Polynomials *) + +type deg = int +type coef = P.t +type poly + +val repr : poly -> (coef * int array) 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 + +module Hashpol : Hashtbl.S with type key = poly + +val sugar_flag : bool ref +val divide_rem_with_critical_pair : bool ref + +end + +exception NotInIdeal + +val lexico : bool ref |