diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ae66791b0c..4f46a80dcf 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -181,7 +181,7 @@ rules. Some simple left factorization work has to be done. Here is an example. .. coqtop:: all Notation "x < y" := (lt x y) (at level 70). - Notation "x < y < z" := (x < y /\ y < z) (at level 70). + Fail Notation "x < y < z" := (x < y /\ y < z) (at level 70). In order to factorize the left part of the rules, the subexpression referred to by ``y`` has to be at the same level in both rules. However the @@ -486,7 +486,7 @@ Sometimes, for the sake of factorization of rules, a binder has to be parsed as a term. This is typically the case for a notation such as the following: -.. coqtop:: in +.. coqdoc:: Notation "{ x : A | P }" := (sig (fun x : A => P)) (at level 0, x at level 99 as ident). @@ -788,9 +788,9 @@ main grammar, or from another custom entry as is the case in to indicate that ``e`` has to be parsed at level ``2`` of the grammar associated to the custom entry ``expr``. The level can be omitted, as in -.. coqtop:: in +.. coqdoc:: - Notation "[ e ]" := e (e custom expr)`. + Notation "[ e ]" := e (e custom expr). in which case Coq tries to infer it. @@ -1058,7 +1058,7 @@ Binding arguments of a constant to an interpretation scope in the scope delimited by the key ``F`` (``Rfun_scope``) and the last argument in the scope delimited by the key ``R`` (``R_scope``). - .. coqtop:: in + .. coqdoc:: Arguments plus_fct (f1 f2)%F x%R. @@ -1066,7 +1066,7 @@ Binding arguments of a constant to an interpretation scope parentheses. In the following example arguments A and B are marked as maximally inserted implicit arguments and are put into the type_scope scope. - .. coqtop:: in + .. coqdoc:: Arguments respectful {A B}%type (R R')%signature _ _. @@ -1148,7 +1148,7 @@ Binding types of arguments to an interpretation scope can be bound to an interpretation scope. The command to do it is :n:`Bind Scope @scope with @class` - .. coqtop:: in + .. coqtop:: in reset Parameter U : Set. Bind Scope U_scope with U. @@ -1497,12 +1497,12 @@ Numeral notations for only non-negative integers, and the given numeral is negative. - .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first). + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first). The parsing function given to the :cmd:`Numeral Notation` vernacular is not of the right type. - .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first). + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first). The printing function given to the :cmd:`Numeral Notation` vernacular is not of the right type. |