2.2.1

README.md

@@ -42,7 +42,7 @@ that HTT implements Separation logic as a shallow embedding in Coq.
 - Compatible Coq versions: 9.0 or later
 - Additional dependencies:
   - [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
-  - [MathComp ssreflect 2.2 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.4 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
   - [FCSL-PCM 2.2](https://github.com/imdea-software/fcsl-pcm)

coq-htt-core.opam

@@ -31,7 +31,8 @@ variables). The connection reconciles dependent types with effects of state and
 establishes Separation logic as a type theory for such effects. In implementation terms, it means
 that HTT implements Separation logic as a shallow embedding in Coq."""
 
-build: ["dune" "build" "-p" name "-j" jobs]
+build: [make "-C" "htt" "-j%{jobs}%"]
+install: [make "-C" "htt" "install"]
 depends: [
   "dune" {>= "3.6"}
   "coq" { (>= "9.0" & < "9.1~") | (= "dev") }

examples/Make

@@ -0,0 +1,29 @@
+-Q . htt
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -redundant-canonical-projection
+
+# release-specific arguments
+-arg -w -arg -notation-incompatible-prefix # specific to coq8.20.0 
+-arg -w -arg -deprecated-from-Coq # specific to coq8.21 
+-arg -w -arg -deprecated-dirpath-Coq # specific to coq8.21 
+
+exploit.v
+gcd.v
+counter.v
+llist.v
+dlist.v
+array.v
+queue.v
+cyclic.v
+stack.v
+bintree.v
+bst.v
+kvmaps.v
+hashtab.v
+bubblesort.v
+quicksort.v
+congmath.v
+congprog.v
+tree.v	
+union_find.v

examples/Makefile

@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../Makefile.common

examples/dune

@@ -0,0 +1,9 @@
+(coq.theory
+ (name htt)
+ (package coq-htt)
+ (synopsis "Hoare Type Theory with examples")
+ (flags :standard
+   -w -notation-overridden
+   -w -local-declaration
+   -w -redundant-canonical-projection
+   -w -projection-no-head-constant))

htt/Make

@@ -0,0 +1,14 @@
+-Q . htt
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -redundant-canonical-projection
+
+# release-specific arguments
+-arg -w -arg -notation-incompatible-prefix # specific to coq8.20.0 
+-arg -w -arg -deprecated-from-Coq # specific to coq8.21 
+-arg -w -arg -deprecated-dirpath-Coq # specific to coq8.21 
+
+options.v
+domain.v
+model.v
+heapauto.v

htt/Makefile

@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../Makefile.common

htt/dune

@@ -0,0 +1,11 @@
+; This file was generated from `meta.yml`, please do not edit manually.
+
+(coq.theory
+ (name htt)
+ (package coq-htt-core)
+ (synopsis "Hoare Type Theory")
+ (flags :standard
+   -w -notation-overridden
+   -w -local-declaration
+   -w -redundant-canonical-projection
+   -w -projection-no-head-constant))

meta.yml

@@ -100,7 +100,7 @@ dependencies:
     name: coq-mathcomp-ssreflect
     version: '{ (>= "2.4.0" & < "2.5~") | (= "dev") }'
   description: |-
-    [MathComp ssreflect 2.2 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.4 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
   description: |-