diff --git a/CHANGES.md b/CHANGES.md
index a14f6017fc98d06b7be57fabfbe2b8e5abe19e49..be26095467a504bd03e0f9320b9ea170bbc45042 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -49,6 +49,7 @@ Provers
   * support for Z3 4.8.1 (released Oct 16, 2018)
   * support for Z3 4.8.3 (released Nov 20, 2018)
   * support for Z3 4.8.4 (released Dec 20, 2018)
+  * support for Coq 8.9.0 (released Jan 17, 2019)
   * upgraded Coq realizations for floating-point arithmetic to Flocq 3.1
 
 Version 1.1.1, December 17, 2018
diff --git a/share/provers-detection-data.conf b/share/provers-detection-data.conf
index c45e3942ad40afd44e0eae817b522b7fda207165..4d0376eb9e39dae7fdd153f783096a677ae1b61e 100644
--- a/share/provers-detection-data.conf
+++ b/share/provers-detection-data.conf
@@ -590,6 +590,7 @@ support_library = "%l/coq/version"
 exec = "coqtop"
 version_switch = "-v"
 version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
+version_ok = "^8\.9\.[0]$"
 version_ok = "^8\.8\.[0-2]$"
 version_ok = "^8\.7\.[0-2]$"
 version_ok = "8.6.1"