fix duplicate-clear warning in recommended way

_CoqProject

@@ -1,6 +1,5 @@
 -Q theories RegLang
 -arg -w -arg -notation-overridden
--arg -w -arg -duplicate-clear
 -arg -w -arg -redundant-canonical-projection
 theories/misc.v
 theories/setoid_leq.v

theories/dfa.v

@@ -338,7 +338,7 @@ Lemma regular_quotR (char : finType) (L1 L2 : lang char) :
 Proof.
   move => [A LA] reg2.
   suff dec_L1 q : decidable (exists2 y, L2 y & delta q y \in dfa_fin A).
-  { exists (dfa_quot dec_L1) => x. apply: (rwP (dfa_quotP _ _ _)) => {x} x. by rewrite LA. }
+  { exists (dfa_quot dec_L1) => x. apply: (rwP (dfa_quotP _ _ _)) => {} x. by rewrite LA. }
   case: reg2 => {LA} [B LB].
   pose C := {| dfa_s := q ; dfa_fin := dfa_fin A ; dfa_trans := @dfa_trans _ A |}.
   pose dec := dfa_inhab (dfa_op andb B C).

theories/dune

@@ -2,4 +2,4 @@
  (name RegLang)
  (package coq-reglang)
  (synopsis "Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp")
- (flags :standard -w -notation-overridden -w -duplicate-clear -w -redundant-canonical-projection))
+ (flags :standard -w -notation-overridden -w -redundant-canonical-projection))

theories/regexp.v

@@ -419,7 +419,7 @@ Section Image.
       + exists [::a] => //. by rewrite /atom inE.
       + by rewrite /atom inE => [[]] /eqP -> <-.
     - apply: (iffP idP) => [/starP [vv] /allP Hvv dev_v|].
-        have {Hvv IHe} Hvv v' : v' \in vv -> image h (re_lang e) v'.
+        have {IHe} Hvv v' : v' \in vv -> image h (re_lang e) v'.
           by move => /Hvv /= /andP [_ /IHe].
         subst v. elim: vv Hvv => [|v vv IHvv] Hvv /=; first by exists [::]; rewrite ?h0.
         case: (Hvv v (mem_head _ _)) => w [Hw1 Hw2].