diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 4 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/implicit-arguments.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 2 |
7 files changed, 13 insertions, 10 deletions
diff --git a/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst b/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst new file mode 100644 index 0000000000..95a9093272 --- /dev/null +++ b/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Undetected collision between a lonely notation and a notation in + scope at printing time + (`#12946 <https://github.com/coq/coq/pull/12946>`_, + fixes the first part of `#12908 <https://github.com/coq/coq/issues/12908>`_, + by Hugo Herbelin). diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 11162ec96b..d533470f22 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -298,7 +298,7 @@ Summary of the commands .. cmd:: Class @inductive_definition {* with @inductive_definition } The :cmd:`Class` command is used to declare a typeclass with parameters - :token:`binders` and fields the declared record fields. + :n:`{* @binder }` and fields the declared record fields. Like any command declaring a record, this command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, @@ -337,7 +337,7 @@ Summary of the commands fields defined by :token:`field_def`, where each field must be a declared field of the class. - An arbitrary context of :token:`binders` can be put after the name of the + An arbitrary context of :n:`{* @binder }` can be put after the name of the instance and before the colon to declare a parameterized instance. An optional priority can be declared, 0 being the highest priority as for :tacn:`auto` hints. If the priority :token:`natural` is not specified, it defaults to the number diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index ee8784fc02..a8a574c861 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -183,11 +183,8 @@ todo_include_todos = False nitpicky = True nitpick_ignore = [ ('token', token) for token in [ - 'binders', 'collection', - 'modpath', 'tactic', - 'destruction_arg', 'bindings', 'induction_clause', 'conversion', diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 768c83150e..f1ed64e52a 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -274,7 +274,7 @@ following rules. .. inference:: Prod-Type \WTEG{T}{s} - s \in \{\SProp, \Type{i}\} + s \in \{\SProp, \Type(i)\} \WTE{\Gamma::(x:T)}{U}{\Type(i)} -------------------------------- \WTEG{∀ x:T,~U}{\Type(i)} diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 765373619f..485dfd964d 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -677,7 +677,7 @@ fixpoint equation can be proved. .. index:: single: Fix_F (term) - single: fix_eq (term) + single: Fix_eq (term) single: Fix_F_inv (term) single: Fix_F_eq (term) @@ -696,7 +696,7 @@ fixpoint equation can be proved. forall (x:A) (r:Acc x), F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r. Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s. - Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y). + Lemma Fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y). End FixPoint. End Well_founded. diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index ca69072cb9..f8375e93ce 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -217,7 +217,7 @@ usual implicit arguments disambiguation syntax. The syntax is also supported in internal binders. For instance, in the following kinds of expressions, the type of each declaration present -in :token:`binders` can be bracketed to mark the declaration as +in :n:`{* @binder }` can be bracketed to mark the declaration as implicit: * :n:`fun (@ident:forall {* @binder }, @type) => @term`, * :n:`forall (@ident:forall {* @binder }, @type), @type`, diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index e05be7c2c2..8e23e61018 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -203,7 +203,7 @@ Generation of inversion principles with ``Derive`` ``Inversion`` This command generates an inversion principle for the :tacn:`inversion ... using ...` tactic. The first :token:`ident` is the name of the generated principle. The second :token:`ident` should be an inductive - predicate, and :token:`binders` the variables occurring in the term + predicate, and :n:`{* @binder }` the variables occurring in the term :token:`term`. This command generates the inversion lemma for the sort :token:`sort` corresponding to the instance :n:`forall {* @binder }, @ident @term`. When applied, it is equivalent to having inverted the instance with the |