upgrade to Dune-Coq 0.8, record dependency on Hierarchy Builder (#59)

README.md

@@ -48,6 +48,7 @@ decidability results and closure properties of regular languages.
 - Compatible Coq versions: 8.16 or later (use releases for other Coq versions)
 - Additional dependencies:
   - [MathComp](https://math-comp.github.io) 2.0 or later (`ssreflect` suffices)
+  - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.4.0 or later
 - Coq namespace: `RegLang`
 - Related publication(s):
   - [Regular Language Representations in the Constructive Type Theory of Coq](https://hal.archives-ouvertes.fr/hal-01832031/document) doi:[10.1007/s10817-018-9460-x](https://doi.org/10.1007/s10817-018-9460-x)

coq-reglang.opam

@@ -21,9 +21,10 @@ decidability results and closure properties of regular languages."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.5"}
+  "dune" {>= "3.8.1"}
   "coq" {>= "8.16"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
+  "coq-hierarchy-builder" {>= "1.4.0"}
 ]
 
 tags: [

dune-project

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

meta.yml

@@ -57,6 +57,11 @@ dependencies:
     version: '{>= "2.0"}'
   description: |-
     [MathComp](https://math-comp.github.io) 2.0 or later (`ssreflect` suffices)
+- opam:
+    name: coq-hierarchy-builder
+    version: '{>= "1.4.0"}'
+  description: |-
+    [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.4.0 or later
 
 tested_coq_opam_versions:
 - version: 'coq-dev'

theories/dune

@@ -2,4 +2,5 @@
  (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 -notation-incompatible-format -w -deprecated-instance-without-locality -w -redundant-canonical-projection))
+ (flags :standard -w -notation-overridden -w -duplicate-clear -w -redundant-canonical-projection)
+ (theories mathcomp.ssreflect HB elpi))

theories/misc.v

@@ -1,6 +1,5 @@
 (* Authors: Christian Doczkal and Jan-Oliver Kaiser *)
 (* Distributed under the terms of CeCILL-B. *)
-Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 
 Set Default Proof Using "Type".