diff --git a/CHANGES.md b/CHANGES.md
index a883358..d4c4d7b 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -3,6 +3,6 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
-## 1.0.0 (2025-01-13)
+## 1.0.0 (2025-01-20)
 
 First release.
diff --git a/README.md b/README.md
index 81c66bd..b1bc2d1 100644
--- a/README.md
+++ b/README.md
@@ -1,13 +1,13 @@
 HOL-Light definition of real numbers in Coq using N
 ---------------------------------------------------
 
-This library provides a translation in Coq of the definition of real numbers in HOL-Light, using the Coq type N for natural numbers.
+This library provides a translation in Coq of the definition of real numbers in HOL-Light, using the Coq type N for natural numbers (it is an adaptation of [coq-hol-light-real-with-nat](https://github.com/Deducteam/coq-hol-light-real-with-nat/)).
 
 It has been automatically generated from HOL-Light using [hol2dk](https://github.com/Deducteam/hol2dk) and [lambdapi](https://github.com/Deducteam/lambdapi).
 
 Proofs are not included but can be regenerated and rechecked by running [reproduce](https://github.com/Deducteam/coq-hol-light-real/blob/main/reproduce) (it takes about 7 minutes on a machine with 32 processors Intel Core i9-13950HX and 64 Gb RAM).
 
-As HOL-Light is based on higher-order logic, this library assumes classical logic, Hilbert's ε operator, functional and propositional extensionnality (see [HOLLight.v](https://github.com/Deducteam/coq-hol-light-real/blob/main/HOLLight.v) for more details):
+As HOL-Light is based on higher-order logic, this library assumes classical logic, Hilbert's ε operator, functional and propositional extensionnality:
 
 ```
 Axiom classic : forall P:Prop, P \/ ~ P.
diff --git a/coq-hol-light-real-with-N.opam b/coq-hol-light-real-with-N.opam
index 2137451..12b2f8e 100644
--- a/coq-hol-light-real-with-N.opam
+++ b/coq-hol-light-real-with-N.opam
@@ -20,6 +20,6 @@ tags: [
   "keyword:HOL-Light"
   "category:Math/Arith/Misc"
   "category:Math/Arith/Real numbers"
-  "date:2024-11-03"
+  "date:2025-01-20"
   "logpath:HOLLight_Real_With_N"
 ]