Merge branch 'v8.6'

6 files changed, 68 insertions, 81 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 312c2eab3d..a980a43f53 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -371,8 +371,7 @@ and extract_really_ind env kn mib =
     let packets =
       Array.mapi
 	(fun i mip ->
-	   let (ind,u), ctx = 
-	     Universes.fresh_inductive_instance env (kn,i) in
+	   let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in
 	   let ar = Inductive.type_of_inductive env ((mib,mip),u) in
 	   let info = (fst (flag_of_type env ar) = Info) in
 	   let s,v = if info then type_sign_vl env ar else [],[] in
@@ -591,10 +590,10 @@ let rec extract_term env mle mlt c args =
 	with NotDefault d ->
 	  let mle' = Mlenv.push_std_type mle (Tdummy d) in
 	  ast_pop (extract_term env' mle' mlt c2 args'))
-    | Const (kn,u) ->
-	extract_cst_app env mle mlt kn u args
-    | Construct (cp,u) ->
-	extract_cons_app env mle mlt cp u args
+    | Const (kn,_) ->
+	extract_cst_app env mle mlt kn args
+    | Construct (cp,_) ->
+	extract_cons_app env mle mlt cp args
     | Proj (p, c) ->
         let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
 	  extract_term env mle mlt term args
@@ -645,7 +644,7 @@ and make_mlargs env e s args typs =
 
 (*s Extraction of a constant applied to arguments. *)
 
-and extract_cst_app env mle mlt kn u args =
+and extract_cst_app env mle mlt kn args =
   (* First, the [ml_schema] of the constant, in expanded version. *)
   let nb,t = record_constant_type env kn None in
   let schema = nb, expand env t in
@@ -718,7 +717,7 @@ and extract_cst_app env mle mlt kn u args =
    they are fixed, and thus are not used for the computation.
    \end{itemize} *)
 
-and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args =
+and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   (* First, we build the type of the constructor, stored in small pieces. *)
   let mi = extract_ind env kn in
   let params_nb = mi.ind_nparams in
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 7c2178222f..48bdad8264 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -19,75 +19,6 @@ open Utile
 
 exception NotInIdeal
 
-module type S = sig
-
-(* Monomials *)
-type mon = int array
-
-val mult_mon : mon -> mon -> mon
-val deg : mon -> int
-val compare_mon : mon -> mon -> int
-val div_mon : mon -> mon -> mon
-val div_mon_test : mon -> mon -> bool
-val ppcm_mon : mon -> mon -> mon
-
-(* Polynomials *)
-
-type deg = int
-type coef
-type poly
-type polynom 
-
-val repr : poly -> (coef * mon) list
-val polconst : coef -> poly
-val zeroP : poly
-val gen : int -> poly
-
-val equal : poly -> poly -> bool
-val name_var : string list ref
-val getvar : string list -> int -> string
-val lstringP : poly list -> string
-val printP : poly -> unit
-val lprintP : poly list -> unit
-
-val div_pol_coef : poly -> coef -> poly
-val plusP : poly -> poly -> poly
-val mult_t_pol : coef -> mon -> poly -> poly
-val selectdiv : mon -> poly list -> poly
-val oppP : poly -> poly
-val emultP : coef -> poly -> poly
-val multP : poly -> poly -> poly
-val puisP : poly -> int -> poly
-val contentP : poly -> coef
-val contentPlist : poly list -> coef
-val pgcdpos : coef -> coef -> coef
-val div_pol : poly -> poly -> coef -> coef -> mon -> poly
-val reduce2 : poly -> poly list -> coef * poly
-
-val poldepcontent : coef list ref
-val coefpoldep_find : poly -> poly -> poly
-val coefpoldep_set : poly -> poly -> poly -> unit
-val initcoefpoldep : poly list -> unit
-val reduce2_trace : poly -> poly list -> poly list -> poly list * poly
-val spol : poly -> poly -> poly
-val etrangers : poly -> poly -> bool
-val div_ppcm : poly -> poly -> poly -> bool
-
-val genPcPf : poly -> poly list -> poly list -> poly list
-val genOCPf : poly list -> poly list
-
-val is_homogeneous : poly -> bool
-
-type certificate =
-    { coef : coef; power : int;
-      gb_comb : poly list list; last_comb : poly list }
-
-val test_dans_ideal : poly -> poly list -> poly list ->
-  poly list * poly * certificate
-val in_ideal : deg -> poly list -> poly -> poly list * poly * certificate
-
-end
-
 (***********************************************************************
    Global options
 *)
diff --git a/plugins/nsatz/ideal.mli b/plugins/nsatz/ideal.mli
new file mode 100644
index 0000000000..d1a2a0a7d1
--- /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
diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli
new file mode 100644
index 0000000000..e876ccfa5d
--- /dev/null
+++ b/plugins/nsatz/nsatz.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+val nsatz_compute : Constr.t -> unit Proofview.tactic
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 96885d2f7a..20022c00ec 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -18,7 +18,6 @@ Require Import BinInt.
 Require Import Setoid.
 Require Export Ncring.
 Require Export Ncring_polynom.
-Import List.
 
 Set Implicit Arguments.
 
@@ -78,7 +77,8 @@ Context {R:Type}`{Ring R}.
   | Z0 => 0
   | Zneg p => -(gen_phiPOS p)
   end.
- Notation "[ x ]" := (gen_phiZ x).
+ Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
+ Local Open Scope ZMORPHISM.
 
  Definition get_signZ z :=
   match z with
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 7fcd6c08a7..f7757a18da 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -238,7 +238,6 @@ Section ALMOST_RING.
  Variable req : R -> R -> Prop.
  Notation "0" := rO.  Notation "1" := rI.
  Infix "==" := req. Infix "+" := radd.  Infix "* " := rmul.
- Infix "-" := rsub. Notation "- x" := (ropp x).
 
  (** Leibniz equality leads to a setoid theory and is extensional*)
  Lemma Eqsth : Equivalence (@eq R).
@@ -263,7 +262,7 @@ Section ALMOST_RING.
         -x = x and x - y = x + y *)
  Definition SRopp (x:R) := x. Notation "- x" := (SRopp x).
 
- Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y).
+ Definition SRsub x y := x + -y. Infix "-" := SRsub.
 
  Lemma SRopp_ext : forall x y, x == y -> -x == -y.
  Proof. intros x y H; exact H. Qed.
@@ -320,6 +319,8 @@ Section ALMOST_RING.
  Qed.
 
  End  SEMI_RING.
+ Infix "-" := rsub.
+ Notation "- x" := (ropp x).
 
  Variable Reqe : ring_eq_ext radd rmul ropp req.
    Add Morphism radd : radd_ext2.  exact (Radd_ext Reqe). Qed.