diff --git a/NIX.md b/NIX.md
index c7ff6cc..0412fbd 100644
--- a/NIX.md
+++ b/NIX.md
@@ -44,5 +44,4 @@
      > nix-shell --arg withEmacs true
 
      in order to get a temporary installation of emacs and
-     proof-general.  Make sure you add `(require 'proof-site)` to your
-     `$HOME/.emacs`.
+     proof-general.
diff --git a/README.md b/README.md
index 579545c..0a9182b 100644
--- a/README.md
+++ b/README.md
@@ -106,16 +106,6 @@ make install
   number of real roots of a polynomial by one plus the number of
   real roots of its derivative,
 
-- `xmathcomp/diag.v` contains the theory of diagonalisation and
-  codiagonalisation with the standard criterions.
-
-- `xmathcomp/mxgal.v` represents elements of a Galois group as
-  matrices, this enables the use of `diag` to find eigenvectors and
-  eigenvalues.
-
-- `xmathcomp/mxextra.v` is a correspondance between `'M_(_,_)` and `'Hom(_, _)`
-   which is unused in the current development, we use `mxgal` instead.
-
 ## Development information
 
 [Developping with nix](NIX.md)
diff --git a/meta.yml b/meta.yml
index 919f851..a825a7e 100644
--- a/meta.yml
+++ b/meta.yml
@@ -148,16 +148,6 @@ documentation: |-
     number of real roots of a polynomial by one plus the number of
     real roots of its derivative,
 
-  - `xmathcomp/diag.v` contains the theory of diagonalisation and
-    codiagonalisation with the standard criterions.
-
-  - `xmathcomp/mxgal.v` represents elements of a Galois group as
-    matrices, this enables the use of `diag` to find eigenvectors and
-    eigenvalues.
-
-  - `xmathcomp/mxextra.v` is a correspondance between `'M_(_,_)` and `'Hom(_, _)`
-     which is unused in the current development, we use `mxgal` instead.
-
   ## Development information
 
   [Developping with nix](NIX.md)