Fix 8.10 warnings.

arthuraa · Aug 13, 2020 · e2ad361 · e2ad361
1 parent ca628ce
commit e2ad361
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 13 deletions.
diff --git a/theories/fmap.v b/theories/fmap.v
@@ -418,7 +418,7 @@ elim: s Ps=> [|p s IH /= Ps] //=.
 rewrite ![in LHS](fun_if, if_arg) /= {}IH; last exact: path_sorted Ps.
 have [-> {k}|k_p] //= := altP (_ =P _); case: (a _)=> //.
 elim: s {Ps} (order_path_min (@Ord.lt_trans _) Ps)
-      => [|p' s IH /andP /= [lb /IH {IH} IH]] //=.
+      => [|p' s IH /andP /= [lb {}/IH IH]] //=.
 by move: lb; have [->|//] := altP (_ =P _); rewrite Ord.ltxx.
 Qed.
 
@@ -630,7 +630,7 @@ Lemma mapm2_comp T T' T'' S S' S'' f f' g g' :
 Proof.
 move=> f_inj f'_inj m; apply/eq_fmap=> x /=.
 have [|xnin] := boolP (x \in domm (mapm2 (f' \o f) (g' \o g) m)).
-- rewrite domm_map2; case/imfsetP=> {x} x xin ->.
+- rewrite domm_map2; case/imfsetP=> {}x xin ->.
   rewrite mapm2E /=; last exact: inj_comp.
   by rewrite !mapm2E //; case: (m x).
 - move: (xnin); rewrite (dommPn xnin).
@@ -684,7 +684,7 @@ apply/(iffP idP).
     apply (sorted_uniq (@Ord.lt_trans T) (@Ord.ltxx T)).
     exact: (valP m).
   rewrite !inE /=; elim: (val m) => [|[k' v'] s IH] //=.
-  move=>/andP [k'_nin_s /IH {IH} IH] /andP [v'_nin_s /IH {IH} IH].
+  move=>/andP [k'_nin_s {}/IH IH] /andP [v'_nin_s {}/IH IH].
   rewrite !inE -pair_eqE /=.
   have [k1k'|k1k'] /= := altP (k1 =P k').
     subst k'; have /negbTE ->: (k1, v) \notin s.
@@ -695,7 +695,7 @@ apply/(iffP idP).
       apply: contra v'_nin_s => v'_in_s.
       by apply/mapP; exists (k2, v).
     by rewrite orbF => /eqP ->.
-  move=> k1_in_s; move: (k1_in_s)=> /IH {IH} IH.
+  move=> k1_in_s; move: (k1_in_s)=> {}/IH IH.
   have [k2k'|k2k'] //= := altP (k2 =P k').
   subst k'; case/orP=> [/eqP ?|//]; subst v'.
   suff c : v \in unzip2 s by rewrite c in v'_nin_s.

diff --git a/theories/fperm.v b/theories/fperm.v
@@ -86,6 +86,7 @@ End FPerm.
 
 Export FPerm.Exports.
 
+Declare Scope fperm_scope.
 Delimit Scope fperm_scope with fperm.
 
 Definition fun_of_fperm T (s : FPerm.fperm_type T) x :=
@@ -250,7 +251,7 @@ have st: fperm_def @: (X :|: f @: X) = X :|: f @: X.
         move=> n; elim=> [|n' IH]; first by rewrite leqn0=> _ /eqP->.
         rewrite leq_eqVlt=> nin /orP [/eqP-> //|]; rewrite ltnS=> lnn'.
         by rewrite (erefl : g n'.+1 = f' (g n')) IH // /f' (negbTE nin).
-      have {sub} sub: fsubset (g @: S) X.
+      have {}sub: fsubset (g @: S) X.
         apply/fsubsetP=> x' /imfsetP [n]; rewrite {1}/S in_fset mem_iota.
         rewrite leq0n /= add0n ltnS => Hn -> {x'}.
         by apply: contraTT it_in=> g_nin; rewrite (sub _ _ g_nin Hn).

diff --git a/theories/fset.v b/theories/fset.v
@@ -59,7 +59,7 @@ Record fset_type := FSet {
 Lemma fset_subproof (s : seq T) :
   sorted (@Ord.lt T) (sort (@Ord.leq T) (undup s)).
 Proof.
-move: (undup s) (undup_uniq s)=> {s} s.
+move: (undup s) (undup_uniq s)=> {}s.
 move/permPl/perm_uniq: (perm_sort (@Ord.leq T) s)=> <- u_s.
 move: {s} (sort _ _) u_s (sort_sorted (@Ord.leq_total T) s)=> [|x s] //=.
 case/andP; elim: s x => //= x' s IH x; rewrite inE negb_or Ord.leq_eqVlt.
@@ -107,6 +107,7 @@ End FSet.
 
 Export FSet.Exports.
 
+Declare Scope fset_scope.
 Delimit Scope fset_scope with fset.
 
 Lemma fset_key : unit. Proof. exact: tt. Qed.
@@ -813,7 +814,7 @@ Lemma bigcup_sup j s P F :
 Proof.
 elim: s=> [|j' s IH] //=; rewrite inE=> /orP [/eqP <-|]; rewrite big_cons.
   by move=> ->; rewrite fsubsetUl.
-case: ifP => // _ /IH {IH} IH /IH {IH} IH.
+case: ifP => // _ {}/IH IH {}/IH IH.
 by rewrite (fsubset_trans IH) // fsubsetUr.
 Qed.
 
@@ -921,7 +922,7 @@ Lemma imfsetI f s1 s2 :
   {in s1 & s2, injective f} -> f @: (s1 :&: s2) = f @: s1 :&: f @: s2.
 Proof.
 move=> inj; apply/eq_fset=> x; apply/imfsetP/fsetIP.
-  case=> [{x} x x_in ->]; case/fsetIP: x_in=> [x_in1 x_in2].
+  case=> [{}x x_in ->]; case/fsetIP: x_in=> [x_in1 x_in2].
   by apply/andP; rewrite ?mem_imfset.
 case=> [/imfsetP [y1 y1_in ->] /imfsetP [y2 y2_in]] e.
 by exists y1; rewrite // in_fsetI y1_in /= (inj _ _ y1_in y2_in e).
@@ -931,8 +932,8 @@ Lemma imfset_fset f xs : f @: fset xs = fset [seq f x | x <- xs].
 Proof.
 apply/eq_fset=> x; rewrite in_fset.
 apply/(sameP imfsetP)/(iffP mapP).
-- by case=> {x} x xin ->; exists x; rewrite ?in_fset.
-- by case=> {x} x xin ->; exists x; rewrite -1?in_fset.
+- by case=> {}x xin ->; exists x; rewrite ?in_fset.
+- by case=> {}x xin ->; exists x; rewrite -1?in_fset.
 Qed.
 
 Lemma imfset_eq0 f X : (f @: X == fset0) = (X == fset0).

diff --git a/theories/ord.v b/theories/ord.v
@@ -41,6 +41,7 @@ Unset Printing Implicit Defensive.
 
 (* Interface of types with an order relation. *)
 
+Declare Scope ord_scope.
 Delimit Scope ord_scope with ord.
 
 Module Ord.
@@ -484,7 +485,7 @@ have anti: antisymmetric tree_leq.
     case: eqP=> [->|] //; rewrite eqxx ltnn /= => H.
     rewrite (_ : s1 = s2) //.
     elim: s1 s2 IH H {l21 n1 n2} => [|t1 s1 IH] [|t2 s2] //=.
-    case=> anti_t1 /IH {IH} IH.
+    case=> anti_t1 {}/IH IH.
     by rewrite [t2 == _]eq_sym; case: eqP=> [-> /IH ->|_ /anti_t1] //.
   by rewrite gtn_eqF //= ltnNge ltnW //=.
 split=> //.
@@ -501,15 +502,15 @@ split=> //.
   case/orP=> [->|/andP [-> e23]] //=.
   apply/orP; right.
   elim: s2 s1 s3 IH e12 e23=> [|t2 s2 IH] [|t1 s1] [|t3 s3] //=.
-  case=> t2_trans /IH {IH} IH.
+  case=> t2_trans {}/IH IH.
   case: ifPn => [/eqP <-|ne12]; first by case: eqP; eauto.
   case: ifPn => [/eqP <-|ne23]; first by rewrite (negbTE ne12).
   move: ne12 ne23; case: (t1 =P t3) => [<-|]; last by eauto.
   move=> ne _ l12 l21; move: (anti t1 t2) ne; rewrite l12 l21.
   by move=> /(_ erefl) ->; rewrite eqxx.
 - elim=> [x1|n1 s1 IH] [x2|n2 s2] //=; first exact: Ord.leq_total.
   case: ltngtP=> //= _.
-  elim: s1 s2 IH {n1 n2}=> [|t1 s1 IH] [|t2 s2] //= [total_t1 /IH {IH} IH].
+  elim: s1 s2 IH {n1 n2}=> [|t1 s1 IH] [|t2 s2] //= [total_t1 {}/IH IH].
   by rewrite [t2 == _]eq_sym; case: (t1 =P t2)=> //.
 Qed.