diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 16 |
2 files changed, 8 insertions, 21 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 0f255e4e64..4e8a2b0879 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -100,19 +100,6 @@ processed color, though their preceding proofs have the processed color. Notice that for all these buttons, except for the "gears" button, their operations are also available in the menu, where their keyboard shortcuts are given. -Proof folding ------------------- - -As your script grows bigger and bigger, it might be useful to hide the -proofs of your theorems and lemmas. - -This feature is toggled via the Hide entry of the Navigation menu. The -proof shall be enclosed between ``Proof.`` and ``Qed.``, both with their final -dots. The proof that shall be hidden or revealed is the first one -whose beginning statement (such as ``Theorem``) precedes the insertion -cursor. - - Vernacular commands, templates ----------------------------------- diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 921c7bbbf7..bc77e2e58c 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -245,9 +245,9 @@ file timing data: COQDEP Fast.v COQDEP Slow.v COQC Slow.v - Slow (user: 0.34 mem: 395448 ko) + Slow.vo (user: 0.34 mem: 395448 ko) COQC Fast.v - Fast (user: 0.01 mem: 45184 ko) + Fast.vo (user: 0.01 mem: 45184 ko) + ``pretty-timed`` this target stores the output of ``make TIMED=1`` into @@ -280,15 +280,15 @@ file timing data: COQDEP Fast.v COQDEP Slow.v COQC Slow.v - Slow (user: 0.36 mem: 393912 ko) + Slow.vo (user: 0.36 mem: 393912 ko) COQC Fast.v - Fast (user: 0.05 mem: 45992 ko) + Fast.vo (user: 0.05 mem: 45992 ko) Time | File Name -------------------- 0m00.41s | Total -------------------- - 0m00.36s | Slow - 0m00.05s | Fast + 0m00.36s | Slow.vo + 0m00.05s | Fast.vo + ``print-pretty-timed-diff`` @@ -338,8 +338,8 @@ file timing data: -------------------------------------------------------- 0m00.39s | Total | 0m00.35s || +0m00.03s | +11.42% -------------------------------------------------------- - 0m00.37s | Slow | 0m00.01s || +0m00.36s | +3600.00% - 0m00.02s | Fast | 0m00.34s || -0m00.32s | -94.11% + 0m00.37s | Slow.vo | 0m00.01s || +0m00.36s | +3600.00% + 0m00.02s | Fast.vo | 0m00.34s || -0m00.32s | -94.11% The following targets and ``Makefile`` variables allow collection of per- |