From 8aa06ae3604852ee67b7316c8a2bef7f2e754e49 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Thu, 3 Aug 2023 15:17:03 +0200
Subject: [PATCH] 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 -
 coq-reglang.opam  | 5 +----
 dune-project      | 4 ++--
 theories/dfa.v    | 2 +-
 theories/dune     | 3 +--
 theories/regexp.v | 2 +-
 6 files changed, 6 insertions(+), 11 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index dbf4cc5..ca4359c 100644
--- a/_CoqProject
+++ b/_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
diff --git a/coq-reglang.opam b/coq-reglang.opam
index f556c79..8470a68 100644
--- a/coq-reglang.opam
+++ b/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: "palmskog@gmail.com"
 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"}
diff --git a/dune-project b/dune-project
index 1fa6601..855139f 100644
--- a/dune-project
+++ b/dune-project
@@ -1,3 +1,3 @@
-(lang dune 3.8)
-(using coq 0.8)
+(lang dune 2.8)
+(using coq 0.3)
 (name reglang)
diff --git a/theories/dfa.v b/theories/dfa.v
index 4895593..157a7c9 100644
--- a/theories/dfa.v
+++ b/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).
diff --git a/theories/dune b/theories/dune
index fa57b48..e529d33 100644
--- a/theories/dune
+++ b/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))
diff --git a/theories/regexp.v b/theories/regexp.v
index 3daae77..43aefc5 100644
--- a/theories/regexp.v
+++ b/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].