Review #2

Author: jfehrle

doc/sphinx/language/core/basic.rst

@@ -160,15 +160,15 @@ Numbers
 
       .. coqtop:: all reset
 
-         Fail Compute 100000 + 100000.  (* gives a stack overflow (not shown) *)
+         Fail Eval compute in 100000 + 100000.  (* gives a stack overflow (not shown) *)
 
       .. coqtop:: in
 
          Require Import ZArith.  (* for definition of Z *)
 
       .. coqtop:: all
 
-         Compute (1000000000000000000000000000000000 + 1)%Z.
+         Eval compute in (1000000000000000000000000000000000 + 1)%Z.
 
 Strings
   Strings begin and end with ``"`` (double quote).  Use ``""`` to represent

doc/sphinx/user-extensions/syntax-extensions.rst

@@ -2041,8 +2041,8 @@ Number notations
 
       :n:`abstract after @bignat`
          returns :n:`(@qualid__parse m)` when parsing a literal
-         :n:`m` that's greater than :n:`@bignat` rather than reducing it to a normal form.
-         Here :g:`m` will be a
+         :n:`m` that's greater than or equal to :n:`@bignat` rather than reducing
+         it to a normal form.  Here :g:`m` will be a
          :g:`Number.int`, :g:`Number.uint`, :g:`Z` or :g:`Number.number`, depending on the
          type of the parsing function :n:`@qualid__parse`. This allows for a
          more compact representation of literals in types such as :g:`nat`,