Fix #10831: minor issues in documentation of Function.

1 files changed, 14 insertions, 5 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index dc4f91e66b..2d047a1058 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -638,7 +638,11 @@ the induction principle to easily reason about the function.
 
    than like this:
 
-   .. coqtop:: reset all
+   .. coqtop:: reset none
+
+      Require Import FunInd.
+
+   .. coqtop:: all
 
       Function plus (n m : nat) {struct n} : nat :=
       match n with
@@ -649,17 +653,22 @@ the induction principle to easily reason about the function.
 
 *Limitations*
 
-|term_0| must be built as a *pure pattern matching tree* (:g:`match … with`)
+:token:`term` must be built as a *pure pattern matching tree* (:g:`match … with`)
 with applications only *at the end* of each branch.
 
 Function does not support partial application of the function being
 defined. Thus, the following example cannot be accepted due to the
 presence of partial application of :g:`wrong` in the body of :g:`wrong`:
 
-.. coqtop:: all
+.. coqtop:: none
+
+   Require List.
+   Import List.ListNotations.
+
+.. coqtop:: all fail
 
-   Fail Function wrong (C:nat) : nat :=
-   List.hd 0 (List.map wrong (C::nil)).
+   Function wrong (C:nat) : nat :=
+     List.hd 0 (List.map wrong (C::nil)).
 
 For now, dependent cases are not treated for non structurally
 terminating functions.