diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 8 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 5d300c3d6d..19995520bb 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -21,16 +21,16 @@ The most basic custom toplevel is built using: % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ -package coq.toplevel \ - toplevel/coqtop\_bin.ml -o my\_toplevel.native + topbin/coqtop_bin.ml -o my_toplevel.native -For example, to statically link |L_tac|, you can just do: +For example, to statically link |Ltac|, you can just do: :: % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ - -package coq.toplevel -package coq.ltac \ - toplevel/coqtop\_bin.ml -o my\_toplevel.native + -package coq.toplevel,coq.plugins.ltac \ + topbin/coqtop_bin.ml -o my_toplevel.native and similarly for other plugins. diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 0fa42cadad..4cbf75b715 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -600,8 +600,8 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Compat/AdmitAxiom.v - theories/Compat/Coq86.v theories/Compat/Coq87.v theories/Compat/Coq88.v + theories/Compat/Coq89.v </dd> </dl> |