diff --git a/CHANGELOG b/CHANGELOG
index 4e4e69f..3d6296a 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,9 @@
+== RelationAlgebra 1.7.4  (2020, October 20th) ==
+
+- compatibility with Coq 8.11 & 8.12
+- optional dependency on coq-aac-tactics (module [rewriting_aac])
+- a few compilation warnings removed
+
 == RelationAlgebra 1.7.3  (2020, February 27th) ==
 
 - compatibility with Coq 8.11
diff --git a/_CoqProject b/_CoqProject
index d99f2b6..b8001fd 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -79,3 +79,4 @@ all.v
 compiler_opts.v
 imp.v
 paterson.v
+rewriting_aac.v
diff --git a/index.html b/index.html
index 0625c56..aa560cb 100644
--- a/index.html
+++ b/index.html
@@ -248,9 +248,7 @@ <h3 id="doc:tac">Provided tactics</h3>
   <li> Rewriting tactics:
   <ul>
     <li> <code>mrewrite</code>: rewriting modulo associativity of
-    composition (ad-hoc tactic);
-    <li> the library interfaces with <code>AAC_tactics</code>,
-    to obtain more powerful AC rewriting tools.
+    composition (ad-hoc tactic); more AC rewriting tools are available using the <code>AAC_tactics</code> library.
   </ul>  
   <li> Other tactics:
   <ul>
diff --git a/opam b/opam
index 8762f8d..d96edbc 100644
--- a/opam
+++ b/opam
@@ -1,9 +1,11 @@
 opam-version: "2.0"
-name: "coq-relation-algebra"
 synopsis: "Relation Algebra and KAT in Coq"
+name: "coq-relation-algebra"
 maintainer: "Damien Pous <Damien.Pous@ens-lyon.fr>"
 version: "dev"
 homepage: "http://perso.ens-lyon.fr/damien.pous/ra/"
+dev-repo: "git+https://github.com/damien-pous/relation-algebra.git"
+bug-reports: "https://github.com/damien-pous/relation-algebra/issues"
 license: "LGPL"
 depends: [
   "ocaml"