Fix warnings

Author: strub

_CoqProject

@@ -1 +1,6 @@
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -notation-overridden
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -projection-no-head-constant
+
 -R _build/default/src SsrMultinomials

src/dune

@@ -4,6 +4,4 @@
  (flags -w -ambiguous-paths
         -w -notation-overridden
         -w -redundant-canonical-projection
-        -w -projection-no-head-constant
-        -w -duplicate-clear
-        -w -undeclared-scope))
+        -w -projection-no-head-constant))

src/freeg.v

@@ -44,9 +44,11 @@ Local Notation simpm := Monoid.simpm.
 Reserved Notation "{ 'freeg' K / G }" (at level 0, K, G at level 2, format "{ 'freeg'  K  /  G }").
 Reserved Notation "{ 'freeg' K }" (at level 0, K at level 2, format "{ 'freeg'  K }").
 Reserved Notation "[ 'freeg' S ]" (at level 0, S at level 2, format "[ 'freeg'  S ]").
+Reserved Notation "<< z *p k >>"  (at level 0, format "<< z *p k >>").
+Reserved Notation "<< k >>"  (at level 0, format "<< k >>").
 
 (* -------------------------------------------------------------------- *)
-Let perm_eq_map (T U : eqType) (f : T -> U) (xs ys : seq T):
+Lemma perm_eq_map (T U : eqType) (f : T -> U) (xs ys : seq T):
   perm_eq xs ys -> (perm_eq (map f xs) (map f ys)).
 Proof. by move/permP=> h; apply/permP=> p; rewrite !count_map. Qed.
 
@@ -207,7 +209,7 @@ Section FreegTheory.
   Definition dom D := [seq zx.2 | zx <- (repr D)].
 
   Lemma uniq_dom D: uniq (dom D).
-  Proof. by rewrite /dom; case: (repr D)=> /= {D} D; case/andP. Qed.
+  Proof. by rewrite /dom; case: (repr D)=> /= {}D; case/andP. Qed.
 
   Lemma reduced_cons zx s:
     reduced (zx :: s) = [&& zx.1 != 0, zx.2 \notin predom s & reduced s].
@@ -516,7 +518,7 @@ Section FreegTheory.
   Proof.
     apply/esym/eqP/freeg_eqP=> k.
     rewrite -{1 2}[D]freeg_repr !coeff_Freeg /dom.
-    case: (repr D)=> {D} D rD /=; rewrite -map_comp map_id_in //.
+    case: (repr D)=> {}D rD /=; rewrite -map_comp map_id_in //.
     move=> [z x]; rewrite reduced_mem // => /andP [/eqP <- _].
     by rewrite /= coeff_Freeg.
   Qed.

src/monalg.v

@@ -25,6 +25,7 @@ Local Open Scope fset.
 Local Open Scope fmap.
 Local Open Scope ring_scope.
 
+Declare Scope malg_scope.
 Delimit Scope malg_scope with MP.
 
 Local Notation simpm := Monoid.simpm.
@@ -33,6 +34,7 @@ Local Notation ilift := fintype.lift.
 Local Notation efst := (@fst _ _) (only parsing).
 Local Notation esnd := (@snd _ _) (only parsing).
 
+Declare Scope m_scope.
 Delimit Scope m_scope with M.
 
 (* -------------------------------------------------------------------- *)
@@ -53,9 +55,9 @@ Reserved Notation "[ 'malg' x => E ]"
 Reserved Notation "{ 'mpoly' T [ n ] }"
   (at level 0, T, n at level 2, format "{ 'mpoly'  T [ n ] }").
 Reserved Notation "<< z *p k >>"
-  (at level 0).
+  (at level 0, format "<< z *p k >>").
 Reserved Notation "<< k >>"
-  (at level 0).
+  (at level 0, format "<< k >>").
 Reserved Notation "g @_ k"
   (at level 3, k at level 2, left associativity, format "g @_ k").
 Reserved Notation "c %:MP"

src/mpoly.v

@@ -93,6 +93,9 @@ Import Monoid GRing.Theory BigEnough Order.Theory.
 
 Local Open Scope ring_scope.
 
+Declare Scope mpoly_scope.
+Declare Scope multi_scope.
+
 Delimit Scope mpoly_scope with MP.
 Delimit Scope multi_scope with MM.
 
@@ -159,10 +162,10 @@ Hypothesis ih: forall t1, (forall t2, t2 < t1 -> P t2) -> P t1.
 
 Lemma ltxwf t : P t.
 Proof.
-elim: n P ih t => [|k wih] Pn kih t; last case: (tupleP t) => a {t}t.
+elim: n P ih t => [|k wih] Pn kih t; last case: (tupleP t) => a {}t.
   by rewrite tuple0; apply/kih=> t2; rewrite tuple0.
 elim/wf: a t => a iha t; elim/wih: t => t iht.
-apply/kih => t'; case: (tupleP t') => a' {t'}t'; rewrite [_ < _]ltxi_cons.
+apply/kih => t'; case: (tupleP t') => a' {}t'; rewrite [_ < _]ltxi_cons.
 by case: (comparableP a a') => //= [/iha/(_ t')|<- /iht].
 Qed.
 
@@ -761,7 +764,7 @@ elim/(@ltxwf _ [porderType of nat]): t m=> //=; last first.
   move=> t wih m Em; apply/ih=> m' lt_m'm.
   apply/(wih (tof m'))=> //; rewrite -Em.
   by rewrite /tof ltEsub/= -ltEmnm.
-move=> Q {ih} ih x; elim: x {-2}x (leqnn x).
+move=> Q {}ih x; elim: x {-2}x (leqnn x).
   move=> x; rewrite leqn0=> /eqP->; apply/ih.
   by move=> y; rewrite ltEnat/= ltn0.
 move=> k wih l le_l_Sk; apply/ih=> y; rewrite ltEnat => lt_yl.
@@ -2420,7 +2423,7 @@ have: sorted <=%O%O s by apply/sort_sorted/le_total.
 case: s => /= [_|m' s srt_s]; first rewrite perm_sym.
   by move/perm_small_eq=> -> //.
 move/perm_mem => <-; rewrite in_cons => /orP[/eqP->//|].
-elim: s m' srt_s => //= m'' s ih m' /andP[le_mm' /ih {ih}ih].
+elim: s m' srt_s => //= m'' s ih m' /andP[le_mm' /ih {}ih].
 by rewrite in_cons => /orP[/eqP->//|] /ih /(le_trans le_mm').
 Qed.
 
@@ -4112,7 +4115,7 @@ apply/(irr_sorted_eq (leT := ltn))=> //.
   by apply/ltn_trans.
   by move=> ?; rewrite /ltn /= ltnn.
 move=> m; apply/mapP/mapP; case=> /= x;
-  by rewrite (h, =^~ h)=> {h} h ->; exists x.
+  by rewrite (h, =^~ h)=> {}h ->; exists x.
 Qed.
 
 Lemma mesym_tupleE (k : nat) : 's_k =
@@ -4975,7 +4978,7 @@ Lemma homog_prod (s : seq {mpoly R[n]}) :
 Proof.
 move=> homs; apply/homogP; elim: s homs => [_ | p s ihs] /=.
   by exists 0%N; rewrite big_nil; apply/dhomog1.
-case/andP=> /homogP [dp p_hdp] {ihs}/ihs [d ih].
+case/andP=> /homogP [dp p_hdp] {}/ihs [d ih].
 by exists (dp + d)%N; rewrite big_cons; apply/dhomogM.
 Qed.
 

src/ssrcomplements.v

@@ -139,7 +139,7 @@ Section BigMkSub.
       try rewrite filter_uniq // (map_inj_uniq val_inj).
       by rewrite /index_enum -enumT enum_uniq.
     move=> x; rewrite !mem_filter {}/Q; apply/andb_idr.
-    rewrite andbC; case/andP=> /h {h}h /h sT_x.
+    rewrite andbC; case/andP=> /h {}h /h sT_x.
     apply/mapP; exists (Sub x sT_x).
       by rewrite /index_enum -enumT mem_enum.
     by rewrite SubK.