Switch back to Dune-Coq 0.3, fix duplicate-clear warning (#60)

* switch to Dune-Coq 0.3

* 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

coq-reglang.opam

@@ -1,6 +1,3 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-# Follow the instructions on https://github.com/coq-community/templates to regenerate.
-
 opam-version: "2.0"
 maintainer: "[email protected]"
 version: "dev"
@@ -21,7 +18,7 @@ decidability results and closure properties of regular languages."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "3.8.1"}
+  "dune" {>= "2.8"}
   "coq" {>= "8.16"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-hierarchy-builder" {>= "1.4.0"}

dune-project

@@ -1,3 +1,3 @@
-(lang dune 3.8)
-(using coq 0.8)
+(lang dune 2.8)
+(using coq 0.3)
 (name reglang)

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,5 +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)
- (theories mathcomp.ssreflect HB elpi))
+ (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].