documentation fixes

document « Property »

more documentation fixes

[doc] destructed → destructured

[doc] another le_minus→lt_1_r

[doc] @jfehrle suggestions

[doc] more minor fixes

3 files changed, 6 insertions, 6 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 1611e9dd52..c08a9ed0e6 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1147,7 +1147,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
    Polymorphism`.
 
    An inductive type can be forced to be template polymorphic using the
-   ``template`` attribute: it should then fullfill the criterion to
+   ``template`` attribute: it should then fulfill the criterion to
    be template polymorphic or an error is raised.
 
 .. exn:: Inductive @ident cannot be made template polymorphic.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 2d047a1058..f477bf239d 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -182,7 +182,7 @@ other arguments are the parameters of the inductive type.
    recursive (references to the record's name in the type of its field
    raises an  error). To define recursive records, one can use the ``Inductive``
    and ``CoInductive`` keywords, resulting in an inductive or co-inductive record.
-   Definition of mutal inductive or co-inductive records are also allowed, as long
+   Definition of mutually inductive or co-inductive 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.
@@ -1415,7 +1415,7 @@ is needed. In this translation, names in the file system are called
 *physical* paths while |Coq| names are contrastingly called *logical*
 names.
 
-A logical prefix Lib can be associated to a physical pathpath using
+A logical prefix Lib can be associated with a physical path using
 the command line option ``-Q`` `path` ``Lib``. All subfolders of path are
 recursively associated to the logical path ``Lib`` extended with the
 corresponding suffix coming from the physical path. For instance, the
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 2cbd41af8b..ae9d284661 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -111,7 +111,7 @@ Other tokens
   tokens defined at any given time can vary because the :cmd:`Notation`
   command can define new tokens.  A :cmd:`Require` command may load more notation definitions,
   while the end of a :cmd:`Section` may remove notations.  Some notations
-  are defined in the basic library (see :ref:`thecoqlibrary`) and are normallly
+  are defined in the basic library (see :ref:`thecoqlibrary`) and are normally
   loaded automatically at startup time.
 
   Here are the character sequences that Coq directly defines as tokens
@@ -395,7 +395,7 @@ stands for :n:`let @ident := fun {+ @binder} => @term in @term’`.
 Definition by case analysis
 ---------------------------
 
-Objects of inductive types can be destructurated by a case-analysis
+Objects of inductive types can be destructured by a case-analysis
 construction called *pattern matching* expression. A pattern matching
 expression is used to analyze the structure of an inductive object and
 to apply specific treatments accordingly.
@@ -572,7 +572,7 @@ The Vernacular
    assertion          : `assertion_keyword` `ident` [`binders`] : `term` .
    assertion_keyword  : Theorem | Lemma
                       : Remark | Fact
-                      : Corollary | Proposition
+                      : Corollary | Property | Proposition
                       : Definition | Example
    proof              : Proof . … Qed .
                       : Proof . … Defined .