Skip to content

Commit

Permalink
fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Aug 6, 2024
1 parent 3e9bfd3 commit 9a3b857
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 4 deletions.
2 changes: 1 addition & 1 deletion INSTALL.md
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ $ opam install coq-mathcomp-analysis
```
To install a precise version, type, say
```
$ opam install coq-mathcomp-analysis.1.2.0
$ opam install coq-mathcomp-analysis.1.3.0
```
4. Everytime you want to work in this same context, you need to type
```
Expand Down
3 changes: 1 addition & 2 deletions Makefile.common
Original file line number Diff line number Diff line change
Expand Up @@ -129,10 +129,9 @@ doc-clean:

coq2html:
../coq2html/coq2html \
-fragile-mathcomp-break \
-title "Mathcomp Analysis" \
-d html/ -base mathcomp -Q theories analysis \
-coqlib https://coq.inria.fr/doc/V8.18.0/stdlib/ \
-coqlib https://coq.inria.fr/doc/V8.19.2/stdlib/ \
-external https://math-comp.github.io/htmldoc/ mathcomp.ssreflect \
-external https://math-comp.github.io/htmldoc/ mathcomp.algebra \
classical/*.v classical/*.glob \
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ We try to preserve backward compatibility as best as we can.
## Documentation

Each file is documented in its header
([documentation for the last version](https://math-comp.github.io/analysis/htmldoc_1_2_0/index.html), using [`coq2html`](https://github.com/xavierleroy/coq2html)).
([documentation for the last version](https://math-comp.github.io/analysis/htmldoc_1_3_0/index.html), using [`coq2html`](https://github.com/xavierleroy/coq2html)).

Overview presentation: [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018)

Expand Down

0 comments on commit 9a3b857

Please sign in to comment.