Better wording for "Show Proof" and fix typos

3 files changed, 11 insertions, 14 deletions

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 03b30d5d97..57a54bc0ad 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -538,13 +538,11 @@ Requesting information
    .. cmdv:: Show Proof
       :name: Show Proof
 
-      It displays the proof term generated by the tactics
-      that have been applied. If the proof is not completed, this term
-      contain holes, which correspond to the sub-terms which are still to be
-      constructed. These holes appear as a question mark indexed by an
-      integer, and applied to the list of variables in the context, since it
-      may depend on them. The types obtained by abstracting away the context
-      from the type of each placeholder are also printed.
+      Displays the proof term generated by the tactics
+      that have been applied so far. If the proof is incomplete, the term
+      will contain holes, which correspond to subterms which are still to be
+      constructed. Each hole is an existential variable, which appears as a
+      question mark followed by an identifier.
 
    .. cmdv:: Show Conjectures
       :name: Show Conjectures
@@ -574,9 +572,8 @@ Requesting information
    .. cmdv:: Show Existentials
       :name: Show Existentials
 
-      It displays the set of all uninstantiated
-      existential variables in the current proof tree, along with the type
-      and the context of each variable.
+      Displays all open goals / existential variables in the current proof
+      along with the type and the context of each variable.
 
    .. cmdv:: Show Match @ident
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 1d08001e34..75897fec45 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2670,7 +2670,7 @@ context entry name.
      Lemma test n m (H : m + 1 < n) : True.
      have @i : 'I_n by apply: (Sub m); omega.
 
-Note that the sub-term produced by :tacn:`omega` is in general huge and
+Note that the subterm produced by :tacn:`omega` is in general huge and
 uninteresting, and hence one may want to hide it.
 For this purpose the ``[: name ]`` intro pattern and the tactic
 ``abstract`` (see :ref:`abstract_ssr`) are provided.
@@ -4583,7 +4583,7 @@ The ``elim/`` tactic distinguishes two cases:
   passed to the eliminator as the last argument (``x`` in ``foo_ind``) and
   ``en−1 … e1`` are used as patterns to select in the goal the occurrences that
   will be bound by the predicate ``P``, thus it must be possible to unify
-  the sub-term of the goal matched by ``en−1`` with ``pm`` , the one matched
+  the subterm of the goal matched by ``en−1`` with ``pm`` , the one matched
   by ``en−2`` with ``pm−1`` and so on.
 :regular eliminator: in all the other cases. Here it must be possible
   to unify the term matched by ``en`` with ``pm`` , the one matched by
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index bcc5e914ac..a28ce600ca 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -750,12 +750,12 @@ level is otherwise given explicitly by using the syntax
 
 Levels are cumulative: a notation at level ``n`` of which the left end
 is a term shall use rules at level less than ``n`` to parse this
-sub-term. More precisely, it shall use rules at level strictly less
+subterm. More precisely, it shall use rules at level strictly less
 than ``n`` if the rule is declared with ``right associativity`` and
 rules at level less or equal than ``n`` if the rule is declared with
 ``left associativity``. Similarly, a notation at level ``n`` of which
 the right end is a term shall use by default rules at level strictly
-less than ``n`` to parse this sub-term if the rule is declared left
+less than ``n`` to parse this subterm if the rule is declared left
 associative and rules at level less or equal than ``n`` if the rule is
 declared right associative. This is what happens for instance in the
 rule