File tree Expand file tree Collapse file tree 3 files changed +1
-22
lines changed
Expand file tree Collapse file tree 3 files changed +1
-22
lines changed Original file line number Diff line number Diff line change 4444 > nix-shell --arg withEmacs true
4545
4646 in order to get a temporary installation of emacs and
47- proof-general. Make sure you add ` (require 'proof-site) ` to your
48- ` $HOME/.emacs ` .
47+ proof-general.
Original file line number Diff line number Diff line change @@ -106,16 +106,6 @@ make install
106106 number of real roots of a polynomial by one plus the number of
107107 real roots of its derivative,
108108
109- - ` xmathcomp/diag.v ` contains the theory of diagonalisation and
110- codiagonalisation with the standard criterions.
111-
112- - ` xmathcomp/mxgal.v ` represents elements of a Galois group as
113- matrices, this enables the use of ` diag ` to find eigenvectors and
114- eigenvalues.
115-
116- - ` xmathcomp/mxextra.v ` is a correspondance between ` 'M_(_,_) ` and ` 'Hom(_, _) `
117- which is unused in the current development, we use ` mxgal ` instead.
118-
119109## Development information
120110
121111[ Developping with nix] ( NIX.md )
Original file line number Diff line number Diff line change @@ -148,16 +148,6 @@ documentation: |-
148148 number of real roots of a polynomial by one plus the number of
149149 real roots of its derivative,
150150
151- - `xmathcomp/diag.v` contains the theory of diagonalisation and
152- codiagonalisation with the standard criterions.
153-
154- - `xmathcomp/mxgal.v` represents elements of a Galois group as
155- matrices, this enables the use of `diag` to find eigenvectors and
156- eigenvalues.
157-
158- - `xmathcomp/mxextra.v` is a correspondance between `'M_(_,_)` and `'Hom(_, _)`
159- which is unused in the current development, we use `mxgal` instead.
160-
161151 ## Development information
162152
163153 [Developping with nix](NIX.md)
You can’t perform that action at this time.
0 commit comments