diff --git a/README.md b/README.md
index 718479a..c7222bc 100644
--- a/README.md
+++ b/README.md
@@ -12,20 +12,16 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 
 
-This library is a formalization of the mathematics of rigid body
-transformations in the Coq proof-assistant. It can be used to address
-the forward kinematics problem of robot manipulators. It contains
-theories for angles, three-dimensional geometry (including
-three-dimensional rotations, skew-symmetric matrices, quaternions),
-rigid body transformations (isometries, homogeneous representation,
-Denavit-Hartenberg convention, screw motions), and an application to
-the SCARA robot manipulator.
+This repository contains an experimental library for the mathematics
+of rigid body transformations using the Coq proof-assistant and the
+Mathematical Components library.
 
 ## Meta
 
 - Author(s):
   - Reynald Affeldt, AIST (initial)
   - Cyril Cohen, Inria (initial)
+  - Laurent Thery, Inria
 - License: [LGPL-2.1-or-later](LICENSE)
 - Compatible Coq versions: Coq 8.13
 - Additional dependencies:
@@ -66,17 +62,30 @@ Contribution by Damien Rouhling (9b7badc25bf6492f6b84611c7f9d32594b345308)
 
 Grant-in-Aid for Scientific Research Number 15H02687
 
+## Disclaimer
+
+This library is still at an experimental stage.  Contents may change
+and definitions and theorems may be renamed.  Use at your own risk.
+
 ## Documentation
 
-Each file is documented in its header.
+This library can be used to address the forward kinematics problem
+of robot manipulators.  It contains theories for angles,
+three-dimensional geometry (including three-dimensional rotations,
+skew-symmetric matrices, quaternions), rigid body transformations
+(isometries, homogeneous representation, Denavit-Hartenberg
+convention, screw motions), and an application to the SCARA robot
+manipulator.
+
+Each file is documented more precisely in its header.
 
 Some references used in this work:
 - [murray] Murray, Li, Shankar Sastry: A Mathematical Introduction to Robotic Manipulation
 - [springer] Siciliano, Khatib (Eds.): Springer Handbook of Robotics
-- [angeles] Angeles: Fundamentals of Robotic Mechanical Systems
+- [angeles] Angeles: Fundamentals of Robotic Mechanical Systems, Springer 2014
 - [oneill] O'Neill: Elementary Differential Geometry
 - [spong] Spong, Hutchinson, Vidyasagar: Robot Modeling and Control
-- [sciavicco] Sciavicco, L., Siciliano, B.: Modelling and Control of Robot Manipulators
+- [sciavicco] Sciavicco, L., Siciliano, B.: Modelling and Control of Robot Manipulators, Springer 2000
 
 ## Original License
 
diff --git a/coq-robot.opam b/coq-robot.opam
index a60b872..61bc0e0 100644
--- a/coq-robot.opam
+++ b/coq-robot.opam
@@ -12,14 +12,9 @@ license: "LGPL-2.1-or-later"
 
 synopsis: "Formal Foundations for Modeling Robot Manipulators"
 description: """
-This library is a formalization of the mathematics of rigid body
-transformations in the Coq proof-assistant. It can be used to address
-the forward kinematics problem of robot manipulators. It contains
-theories for angles, three-dimensional geometry (including
-three-dimensional rotations, skew-symmetric matrices, quaternions),
-rigid body transformations (isometries, homogeneous representation,
-Denavit-Hartenberg convention, screw motions), and an application to
-the SCARA robot manipulator."""
+This repository contains an experimental library for the mathematics
+of rigid body transformations using the Coq proof-assistant and the
+Mathematical Components library."""
 
 build: [make "-j%{jobs}%" ]
 install: [make "install"]
@@ -42,4 +37,5 @@ tags: [
 authors: [
   "Reynald Affeldt, AIST"
   "Cyril Cohen, Inria"
+  "Laurent Thery, Inria"
 ]
diff --git a/index.md b/index.md
index 2eda026..9b6d42d 100644
--- a/index.md
+++ b/index.md
@@ -20,14 +20,9 @@ header-includes:
 
 Welcome to the Formal Foundations for Modeling Robot Manipulators project website!
 
-This library is a formalization of the mathematics of rigid body
-transformations in the Coq proof-assistant. It can be used to address
-the forward kinematics problem of robot manipulators. It contains
-theories for angles, three-dimensional geometry (including
-three-dimensional rotations, skew-symmetric matrices, quaternions),
-rigid body transformations (isometries, homogeneous representation,
-Denavit-Hartenberg convention, screw motions), and an application to
-the SCARA robot manipulator.
+This repository contains an experimental library for the mathematics
+of rigid body transformations using the Coq proof-assistant and the
+Mathematical Components library.
 
 This is an open source project, licensed under the LGPL-2.1-or-later.
 
@@ -50,4 +45,5 @@ Related publications, if any, are listed below.
 
 - Reynald Affeldt, AIST
 - Cyril Cohen, Inria
+- Laurent Thery, Inria