diff --git a/Makefile b/Makefile
index 3e77020..ad909e5 100644
--- a/Makefile
+++ b/Makefile
@@ -1,16 +1,16 @@
 all: Makefile.coq
-	+$(MAKE) -f Makefile.coq all
+	@+$(MAKE) -f Makefile.coq all
 
 clean: Makefile.coq
-	+$(MAKE) -f Makefile.coq cleanall
-	rm -f Makefile.coq Makefile.coq.conf
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: _CoqProject
 	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-_CoqProject Makefile: ;
+force _CoqProject Makefile: ;
 
-%: Makefile.coq
-	+$(MAKE) -f Makefile.coq $@
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
 
-.PHONY: all clean
+.PHONY: all clean force
diff --git a/README.md b/README.md
index ee3686f..6859f3d 100644
--- a/README.md
+++ b/README.md
@@ -4,6 +4,7 @@
 [![Contributing][contributing-shield]][contributing-link]
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Gitter][gitter-shield]][gitter-link]
+[![coqdoc][coqdoc-shield]][coqdoc-link]
 [![DOI][doi-shield]][doi-link]
 
 [travis-shield]: https://travis-ci.com/coq-community/atbr.svg?branch=master
@@ -18,6 +19,9 @@
 [gitter-shield]: https://img.shields.io/badge/chat-on%20gitter-%23c1272d.svg
 [gitter-link]: https://gitter.im/coq-community/Lobby
 
+[coqdoc-shield]: https://img.shields.io/badge/docs-coqdoc-blue.svg
+[coqdoc-link]: https://coq-community.github.io/atbr/docs/latest/coqdoc/toc.html
+
 [doi-shield]: https://zenodo.org/badge/DOI/10.2168/LMCS-8(1:16)2012.svg
 [doi-link]: https://doi.org/10.2168/LMCS-8(1:16)2012
 
@@ -37,11 +41,10 @@ rather than automata: https://github.com/damien-pous/relation-algebra
   - Damien Pous (initial)
 - Coq-community maintainer(s):
   - Tej Chajed ([**@tchajed**](https://github.com/tchajed))
-  - Karl Palmskog ([**@palmskog**](https://github.com/palmskog))
 - License: [GNU Lesser General Public License v3.0 or later](LICENSE)
 - Compatible Coq versions: 8.11 (use the corresponding branch or release for other Coq versions)
-- Compatible OCaml versions: all versions supported by Coq
-- Additional Coq dependencies: none
+- Compatible OCaml versions: 4.05.0 or later
+- Additional dependencies: none
 - Coq namespace: `ATBR`
 - Related publication(s):
   - [Deciding Kleene Algebras in Coq](https://arxiv.org/abs/1105.4537) doi:[10.2168/LMCS-8(1:16)2012](https://doi.org/10.2168/LMCS-8(1:16)2012)
@@ -68,8 +71,12 @@ make install
 
 ## Documentation
 
-Here is a succinct description of each file.
-The user can also refer to files `Examples.v` and `ChurchRosser.v`.
+The development and underlying theory of the library is described in the paper
+[Deciding Kleene Algebras in Coq][paper], Logical Methods in Computer Science,
+Volume 8, Issue 1, 2012.
+
+Below are succinct descriptions of each file and tactic. See also the
+[coqdoc presentation][coqdoc] of the Coq source files from the latest release.
 
 ### Library files
 
@@ -207,3 +214,6 @@ who participated to a preliminary version of this project. They are also gratefu
 to Assia Mahboubi, Matthieu Sozeau, Bruno Barras, and Hugo Herbelin for highly
 stimulating discussions, as well as numerous hints for solving various problems.
 
+[paper]: https://arxiv.org/abs/1105.4537
+[coqdoc]: https://coq-community.github.io/atbr/docs/latest/coqdoc/toc.html
+
diff --git a/coq-atbr.opam b/coq-atbr.opam
index cadafa9..8b4e3f0 100644
--- a/coq-atbr.opam
+++ b/coq-atbr.opam
@@ -5,9 +5,10 @@ version: "8.11.dev"
 homepage: "https://github.com/coq-community/atbr"
 dev-repo: "git+https://github.com/coq-community/atbr.git"
 bug-reports: "https://github.com/coq-community/atbr/issues"
+doc: "https://coq-community.github.io/atbr/"
 license: "LGPL-3.0-or-later"
 
-synopsis: "A Coq tactic for deciding Kleene algebras"
+synopsis: "Coq library and tactic for deciding Kleene algebras"
 description: """
 This library provides algebraic tools for working with binary relations.
 The main tactic provided is a reflexive tactic for solving (in)equations
@@ -21,7 +22,7 @@ rather than automata: https://github.com/damien-pous/relation-algebra"""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "ocaml"
+  "ocaml" {>= "4.05.0"}
   "coq" {>= "8.11" & < "8.12~"}
 ]
 
diff --git a/meta.yml b/meta.yml
index d108338..e1565a1 100644
--- a/meta.yml
+++ b/meta.yml
@@ -4,9 +4,10 @@ shortname: atbr
 organization: coq-community
 community: true
 travis: true
+coqdoc: true
 doi: 10.2168/LMCS-8(1:16)2012
 
-synopsis: A Coq tactic for deciding Kleene algebras
+synopsis: Coq library and tactic for deciding Kleene algebras
 
 description: |-
   This library provides algebraic tools for working with binary relations.
@@ -32,8 +33,6 @@ authors:
 maintainers:
 - name: Tej Chajed
   nickname: tchajed
-- name: Karl Palmskog
-  nickname: palmskog
 
 opam-file-maintainer: palmskog@gmail.com
 
@@ -43,12 +42,14 @@ license:
   fullname: GNU Lesser General Public License v3.0 or later
   identifier: LGPL-3.0-or-later
 
-plugin: true
-
 supported_coq_versions:
   text: 8.11 (use the corresponding branch or release for other Coq versions)
   opam: '{>= "8.11" & < "8.12~"}'
 
+supported_ocaml_versions:
+    text: 4.05.0 or later
+    opam: '{>= "4.05.0"}'
+
 tested_coq_nix_versions:
 - version_or_url: '8.11'
 
@@ -72,8 +73,12 @@ categories:
 documentation: |
   ## Documentation
 
-  Here is a succinct description of each file.
-  The user can also refer to files `Examples.v` and `ChurchRosser.v`.
+  The development and underlying theory of the library is described in the paper
+  [Deciding Kleene Algebras in Coq][paper], Logical Methods in Computer Science,
+  Volume 8, Issue 1, 2012.
+
+  Below are succinct descriptions of each file and tactic. See also the
+  [coqdoc presentation][coqdoc] of the Coq source files from the latest release.
 
   ### Library files
 
@@ -210,4 +215,7 @@ documentation: |
   who participated to a preliminary version of this project. They are also grateful
   to Assia Mahboubi, Matthieu Sozeau, Bruno Barras, and Hugo Herbelin for highly
   stimulating discussions, as well as numerous hints for solving various problems.
+
+  [paper]: https://arxiv.org/abs/1105.4537
+  [coqdoc]: https://coq-community.github.io/atbr/docs/latest/coqdoc/toc.html
 ---
diff --git a/theories/KleeneAlgebra.v b/theories/KleeneAlgebra.v
index 931a687..b6f7c20 100644
--- a/theories/KleeneAlgebra.v
+++ b/theories/KleeneAlgebra.v
@@ -197,7 +197,9 @@ Section Props2.
   Qed.
 
   Lemma a_star_a_leq_star_a: forall (a: X A A), a*a# <== a#.
-  Proof star_a_a_leq_star_a (KA:=Dual.KleeneAlgebra) (A:=A).
+  Proof.
+    exact (star_a_a_leq_star_a (KA:=Dual.KleeneAlgebra) (A:=A)).
+  Qed.
 
   Lemma star_distr (a b: X A A): (a + b)# == a# * (b*a#)#.
   Proof.
@@ -247,10 +249,14 @@ Section Props3.
   Context `{KA: KleeneAlgebra}.
   
   Lemma semicomm_iter_left: forall A B (a: X A A) (b: X B B) (c: X A B), a*c <== c*b -> a#*c <== c*b#.
-  Proof semicomm_iter_right (KA:=Dual.KleeneAlgebra).
+  Proof.
+    exact (semicomm_iter_right (KA:=Dual.KleeneAlgebra)).
+  Qed.
 
   Lemma wsemicomm_iter_left: forall A (b a : X A A), a*b <== b*a#  ->  a#*b <== b*a#.
-  Proof wsemicomm_iter_right (KA:=Dual.KleeneAlgebra).
+  Proof.
+    exact (wsemicomm_iter_right (KA:=Dual.KleeneAlgebra)).
+  Qed.
 
   Lemma comm_iter_left A B (x : X A B) a b:  a * x == x * b -> a# * x == x * b# .
   Proof.
@@ -272,6 +278,8 @@ Section Props4.
   Context `{KA: KleeneAlgebra}.
   
   Lemma comm_iter_right: forall B A (x : X A B) a b,  x * a == b * x -> x * a# == b# * x .
-  Proof comm_iter_left (KA:=Dual.KleeneAlgebra).
+  Proof.
+    exact (comm_iter_left (KA:=Dual.KleeneAlgebra)).
+  Qed.
 
 End Props4.
diff --git a/theories/MxGraph.v b/theories/MxGraph.v
index b3c763f..23bb4fa 100644
--- a/theories/MxGraph.v
+++ b/theories/MxGraph.v
@@ -49,7 +49,9 @@ Section Defs.
 
   Lemma mx_equal': forall n m (M N: @Classes.X mx_Graph n m) 
     (H: forall i j, i<n -> j<m -> get M i j == get N i j), M == N.
-  Proof (fun _ _ _ _ H => H).
+  Proof.
+    exact (fun _ _ _ _ H => H).
+  Qed.
   
   Definition mx_equal_at p q n m n' m' (M : MX n m) (N : MX n' m') := 
     forall i j, i < p -> j < q -> get M i j == get N i j.
diff --git a/theories/SemiLattice.v b/theories/SemiLattice.v
index 57f3efa..78af28e 100644
--- a/theories/SemiLattice.v
+++ b/theories/SemiLattice.v
@@ -202,7 +202,9 @@ Section Props1.
   Variables A B: T.
   
   Lemma zero_inf: forall (x: X A B), 0 <== x.
-  Proof (@plus_neutral_left _ _ _ A B).  
+  Proof.
+    exact (@plus_neutral_left _ _ _ A B).
+  Qed.
   
   Lemma plus_make_left: forall (x y: X A B), x <== x+y.
   Proof. intros; unfold leq. rewrite plus_assoc, plus_idem. reflexivity. Qed.
diff --git a/theories/Utils_WF.v b/theories/Utils_WF.v
index 564df31..9359748 100644
--- a/theories/Utils_WF.v
+++ b/theories/Utils_WF.v
@@ -80,6 +80,7 @@ Section wf_to.
     rel_to_intro: forall a' a, R a' a -> rel_to (f a') (f a).
   Hypothesis HR: well_founded rel_to.
   Theorem rel_to_wf: well_founded R.
+  Proof.
     intro a. remember (f a) as fa. revert a Heqfa.
     induction fa as [fa IHa] using (well_founded_induction HR).
     constructor. intros a' H. subst. eapply IHa; trivial. constructor. trivial.
@@ -102,7 +103,7 @@ Section wf_lexico_incl.
     intros [a' b'] [a b] [u' u Hab]. auto. 
   Qed.
 End wf_lexico_incl.
-   
+
 
 (** Lazy partial fixpoint operators (lazy iterator):
     we use these functions to avoid the computation of a (2^n) worst-case