Review #2

doc/sphinx/addendum/implicit-coercions.rst

@@ -379,7 +379,7 @@ replaced by ``x:A'`` where ``A'`` is the result of the application to
 ``A`` of the coercion path between the class of ``A`` and
 ``Sortclass`` if it exists.  This case occurs in the abstraction
 :g:`fun x:A => t`, universal quantification :g:`forall x:A,B`, global
-variables and parameters of (co-)inductive definitions and
+variables and parameters of (co)inductive definitions and
 functions. In :g:`forall x:A,B`, such a coercion path may also be applied
 to ``B`` if necessary.
 

doc/sphinx/addendum/universe-polymorphism.rst

@@ -178,7 +178,7 @@ Cumulative, NonCumulative
 .. attr:: universes(cumulative{? = {| yes | no } })
    :name: universes(cumulative); Cumulative; NonCumulative
 
-   Polymorphic inductive types, co-inductive types, variants and
+   Polymorphic inductive types, coinductive types, variants and
    records can be declared cumulative using this :term:`boolean attribute`
    or the legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as
    shown in the examples, is more commonly used.

doc/sphinx/changes.rst

@@ -1672,7 +1672,7 @@ Notations
   by Pierre Roux).
 - **Added:**
   Notations declared with the ``where`` clause in the declaration of
-  inductive types, co-inductive types, record fields, fixpoints and
+  inductive types, coinductive types, record fields, fixpoints and
   cofixpoints now support the ``only parsing`` modifier
   (`#11602 <https://github.com/coq/coq/pull/11602>`_,
   by Hugo Herbelin).
@@ -8513,7 +8513,7 @@ reason on the inductive structure of recursively defined functions.
 Jean-Marc Notin significantly contributed to the general maintenance of
 the system. He also took care of ``coqdoc``.
 
-Pierre Castéran contributed to the documentation of (co-)inductive types
+Pierre Castéran contributed to the documentation of (co)inductive types
 and suggested improvements to the libraries.
 
 Pierre Corbineau implemented a declarative mathematical proof language,
@@ -8764,7 +8764,7 @@ Language and commands
 
 - Added sort-polymorphism for definitions in Type (but finally abandoned).
 - Support for implicit arguments in the types of parameters in
-  (co-)fixpoints and (co-)inductive declarations.
+  (co)fixpoints and (co)inductive declarations.
 - Improved type inference: use as much of possible general information.
   before applying irreversible unification heuristics (allow e.g. to
   infer the predicate in "(exist _ 0 (refl_equal 0) : {n:nat | n=0 })").

doc/sphinx/language/cic.rst

@@ -140,7 +140,7 @@ A :term:`global environment` is an ordered list of *declarations*.
 Global declarations are either *assumptions*, *definitions*
 or declarations of inductive objects. Inductive
 objects declare both constructors and inductive or
-co-inductive types (see Section :ref:`inductive-definitions`).
+coinductive types (see Section :ref:`inductive-definitions`).
 
 In the global environment,
 *assumptions* are written as

doc/sphinx/language/coq-library.rst

@@ -752,7 +752,7 @@ subdirectories:
   * **ZArith** : Basic relative integer arithmetic
   * **Numbers** : Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2^31 binary words)
   * **Bool** : Booleans (basic functions and results)
-  * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types)
+  * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with coinductive types)
   * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.)
   * **FSets** : Specification and implementations of finite sets and finite maps (by lists and by AVL trees)
   * **Reals** : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...)

doc/sphinx/language/core/coinductive.rst

@@ -1,7 +1,7 @@
-Co-inductive types and co-recursive functions
+Co-inductive types and corecursive functions
 =============================================
 
-.. _co-inductive-types:
+.. _coinductive-types:
 
 Co-inductive types
 ------------------
@@ -14,16 +14,16 @@ constructors. Infinite objects are introduced by a non-ending (but
 effective) process of construction, defined in terms of the constructors
 of the type.
 
-More information on co-inductive definitions can be found in
+More information on coinductive definitions can be found in
 :cite:`Gimenez95b,Gim98,GimCas05`.
 
 .. cmd:: CoInductive @inductive_definition {* with @inductive_definition }
 
-   This command introduces a co-inductive type.
+   This command introduces a coinductive type.
    The syntax of the command is the same as the command :cmd:`Inductive`.
-   No principle of induction is derived from the definition of a co-inductive
+   No principle of induction is derived from the definition of a coinductive
    type, since such principles only make sense for inductive types.
-   For co-inductive types, the only elimination principle is case analysis.
+   For coinductive types, the only elimination principle is case analysis.
 
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(template)`, :attr:`universes(cumulative)`,
@@ -36,7 +36,7 @@ More information on co-inductive definitions can be found in
 .. example::
 
    The type of infinite sequences of natural numbers, usually called streams,
-   is an example of a co-inductive type.
+   is an example of a coinductive type.
 
    .. coqtop:: in
 
@@ -50,12 +50,12 @@ More information on co-inductive definitions can be found in
       Definition hd (x:Stream) := let (a,s) := x in a.
       Definition tl (x:Stream) := let (a,s) := x in s.
 
-Definitions of co-inductive predicates and blocks of mutually
-co-inductive definitions are also allowed.
+Definitions of coinductive predicates and blocks of mutually
+coinductive definitions are also allowed.
 
 .. example::
 
-   The extensional equality on streams is an example of a co-inductive type:
+   The extensional equality on streams is an example of a coinductive type:
 
    .. coqtop:: in
 
@@ -71,16 +71,16 @@ co-inductive definitions are also allowed.
 Caveat
 ~~~~~~
 
-The ability to define co-inductive types by constructors, hereafter called
-*positive co-inductive types*, is known to break subject reduction. The story is
+The ability to define coinductive types by constructors, hereafter called
+*positive coinductive types*, is known to break subject reduction. The story is
 a bit long: this is due to dependent pattern-matching which implies
 propositional η-equality, which itself would require full η-conversion for
 subject reduction to hold, but full η-conversion is not acceptable as it would
 make type checking undecidable.
 
 Since the introduction of primitive records in Coq 8.5, an alternative
-presentation is available, called *negative co-inductive types*. This consists
-in defining a co-inductive type as a primitive record type through its
+presentation is available, called *negative coinductive types*. This consists
+in defining a coinductive type as a primitive record type through its
 projections. Such a technique is akin to the *co-pattern* style that can be
 found in e.g. Agda, and preserves subject reduction.
 
@@ -109,15 +109,15 @@ axiom.
 
    Axiom Stream_eta : forall s: Stream, s = Seq (hd s) (tl s).
 
-More generally, as in the case of positive co-inductive types, it is consistent
-to further identify extensional equality of co-inductive types with propositional
+More generally, as in the case of positive coinductive types, it is consistent
+to further identify extensional equality of coinductive types with propositional
 equality:
 
 .. coqtop:: all
 
    Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2.
 
-As of Coq 8.9, it is now advised to use negative co-inductive types rather than
+As of Coq 8.9, it is now advised to use negative coinductive types rather than
 their positive counterparts.
 
 .. seealso::
@@ -140,12 +140,12 @@ Co-recursive functions: cofix
 The expression
 ":n:`cofix @ident__1 @binder__1 : @type__1 with … with @ident__n @binder__n : @type__n for @ident__i`"
 denotes the :math:`i`-th component of a block of terms defined by a mutual guarded
-co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When
+corecursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When
 :math:`n=1`, the ":n:`for @ident__i`" clause is omitted.
 
 .. _cofixpoint:
 
-Top-level definitions of co-recursive functions
+Top-level definitions of corecursive functions
 -----------------------------------------------
 
 .. cmd:: CoFixpoint @cofix_definition {* with @cofix_definition }
@@ -156,19 +156,19 @@ Top-level definitions of co-recursive functions
       cofix_definition ::= @ident_decl {* @binder } {? : @type } {? := @term } {? @decl_notations }
 
    This command introduces a method for constructing an infinite object of a
-   co-inductive type. For example, the stream containing all natural numbers can
+   coinductive type. For example, the stream containing all natural numbers can
    be introduced by applying the following method to the number :g:`O` (see
-   Section :ref:`co-inductive-types` for the definition of :g:`Stream`, :g:`hd`
+   Section :ref:`coinductive-types` for the definition of :g:`Stream`, :g:`hd`
    and :g:`tl`):
 
    .. coqtop:: all
 
       CoFixpoint from (n:nat) : Stream := Seq n (from (S n)).
 
    Unlike recursive definitions, there is no decreasing argument in a
-   co-recursive definition. To be admissible, a method of construction must
+   corecursive definition. To be admissible, a method of construction must
    provide at least one extra constructor of the infinite object for each
-   iteration. A syntactical guard condition is imposed on co-recursive
+   iteration. A syntactical guard condition is imposed on corecursive
    definitions in order to ensure this: each recursive call in the
    definition must be protected by at least one constructor, and only by
    constructors. That is the case in the former definition, where the single
@@ -181,7 +181,7 @@ Top-level definitions of co-recursive functions
       Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream :=
         if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s).
 
-   The elimination of co-recursive definition is done lazily, i.e. the
+   The elimination of corecursive definition is done lazily, i.e. the
    definition is expanded only when it occurs at the head of an application
    which is the argument of a case analysis expression. In any other
    context, it is considered as a canonical expression which is completely

doc/sphinx/language/core/definitions.rst

@@ -150,11 +150,11 @@ The basic assertion command is:
 
    Forms using the :n:`with` clause are useful for theorems that are proved by simultaneous induction
    over a mutually inductive assumption, or that assert mutually dependent
-   statements in some mutual co-inductive type. It is equivalent to
+   statements in some mutual coinductive type. It is equivalent to
    :cmd:`Fixpoint` or :cmd:`CoFixpoint` but using tactics to build the proof of
    the statements (or the :term:`body` of the specification, depending on the point of
-   view). The inductive or co-inductive types on which the induction or
-   co-induction has to be done is assumed to be unambiguous and is guessed by
+   view). The inductive or coinductive types on which the induction or
+   coinduction has to be done is assumed to be unambiguous and is guessed by
    the system.
 
    Like in a :cmd:`Fixpoint` or :cmd:`CoFixpoint` definition, the induction hypotheses

doc/sphinx/language/core/inductive.rst

@@ -370,7 +370,7 @@ recursion. It is the local counterpart of the :cmd:`Fixpoint` command. When
 
 The association of a single fixpoint and a local definition have a special
 syntax: :n:`let fix @ident {* @binder } := @term in` stands for
-:n:`let @ident := fix @ident {* @binder } := @term in`. The same applies for co-fixpoints.
+:n:`let @ident := fix @ident {* @binder } := @term in`. The same applies for cofixpoints.
 
 Some options of :n:`@fixannot` are only supported in specific constructs.  :n:`fix` and :n:`let fix`
 only support the :n:`struct` option, while :n:`wf` and :n:`measure` are only supported in

doc/sphinx/language/core/records.rst

@@ -191,8 +191,8 @@ other arguments are the parameters of the inductive type.
 .. note:: Records defined with the :cmd:`Record` command are not allowed to be
    recursive (references to the record's name in the type of its field
    raises an  error). To define recursive records, one can use the
-   :cmd:`Inductive` and :cmd:`CoInductive` commands, resulting in an inductive or co-inductive record.
-   Definition of mutually inductive or co-inductive records are also allowed, as long
+   :cmd:`Inductive` and :cmd:`CoInductive` commands, resulting in an inductive or coinductive record.
+   Definition of mutually inductive or coinductive records are also allowed, as long
    as all of the types in the block are records.
 
 .. note:: Induction schemes are automatically generated for inductive records.
@@ -221,7 +221,7 @@ other arguments are the parameters of the inductive type.
 .. exn:: Cannot handle mutually (co)inductive records.
 
    Records cannot be defined as part of mutually inductive (or
-   co-inductive) definitions, whether with records only or mixed with
+   coinductive) definitions, whether with records only or mixed with
    standard definitions.
 
 During the definition of the one-constructor inductive definition, all

doc/sphinx/language/extensions/implicit-arguments.rst

@@ -198,7 +198,7 @@ For non-maximally inserted implicit arguments, use square brackets:
 
    Print Implicit map.
 
-For (co-)inductive datatype
+For (co)inductive datatype
 declarations, the semantics are the following: an inductive parameter
 declared as an implicit argument need not be repeated in the inductive
 definition and will become implicit for the inductive type and the constructors.

doc/sphinx/language/extensions/match.rst

@@ -337,7 +337,7 @@ Patterns
 
 The full syntax of `match` is presented in :ref:`match_term`.
 Identifiers in patterns are either constructor names or variables. Any
-identifier that is not the constructor of an inductive or co-inductive
+identifier that is not the constructor of an inductive or coinductive
 type is considered to be a variable. A variable name cannot occur more
 than once in a given pattern. It is recommended to start variable
 names by a lowercase letter.

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -955,7 +955,7 @@ Controlling Typing Flags
 .. flag:: Positivity Checking
 
    This :term:`flag` can be used to enable/disable the positivity checking of inductive
-   types and the productivity checking of co-inductive types. Warning: this can
+   types and the productivity checking of coinductive types. Warning: this can
    break the consistency of the system, use at your own risk. Unchecked
    (co)inductive types are printed by :cmd:`Print Assumptions`.
 

doc/sphinx/proofs/writing-proofs/proof-mode.rst

@@ -886,7 +886,7 @@ Requesting information
 .. cmd:: Guarded
 
    Some tactics (e.g. :tacn:`refine`) allow to build proofs using
-   fixpoint or co-fixpoint constructions. Due to the incremental nature
+   fixpoint or cofixpoint constructions. Due to the incremental nature
    of proof construction, the check of the termination (or
    guardedness) of the recursive calls in the fixpoint or cofixpoint
    constructions is postponed to the time of the completion of the proof.