diff --git a/README.md b/README.md
index a4534b7..ce25e6d 100644
--- a/README.md
+++ b/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)
diff --git a/coq-htt-core.opam b/coq-htt-core.opam
index 1569926..550550b 100644
--- a/coq-htt-core.opam
+++ b/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") }
diff --git a/examples/Make b/examples/Make
new file mode 100644
index 0000000..05db16d
--- /dev/null
+++ b/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
diff --git a/examples/Makefile b/examples/Makefile
new file mode 100644
index 0000000..103b008
--- /dev/null
+++ b/examples/Makefile
@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../Makefile.common
diff --git a/examples/dune b/examples/dune
new file mode 100644
index 0000000..af8c240
--- /dev/null
+++ b/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))
diff --git a/htt/Make b/htt/Make
new file mode 100644
index 0000000..dca3ca7
--- /dev/null
+++ b/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
diff --git a/htt/Makefile b/htt/Makefile
new file mode 100644
index 0000000..103b008
--- /dev/null
+++ b/htt/Makefile
@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../Makefile.common
diff --git a/htt/dune b/htt/dune
new file mode 100644
index 0000000..a6eeaa3
--- /dev/null
+++ b/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))
diff --git a/meta.yml b/meta.yml
index 60b53b6..7c5b946 100644
--- a/meta.yml
+++ b/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: |-