Apply suggestions from code review

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

doc/sphinx/language/core/variants.rst

@@ -40,9 +40,9 @@ Private (matching) inductive types
    the `HoTT library <https://github.com/HoTT/HoTT>`_.
 
    Reducing definitions from the inductive's module can expose
-   :g:`match` to unification, which may result in invalid proof terms.
-   Errors from such terms are delayed until proof completion. Use
-   :cmd:`Validate Proof` to track down which tactic produced the problem term.
+   :g:`match` constructs to unification, which may result in invalid proof terms.
+   Errors from such terms are delayed until proof completion (i.e. on the :cmd:`Qed`). Use
+   :cmd:`Validate Proof` to identify which tactic produced the problematic term.
 
 .. example::
 

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

@@ -1025,11 +1025,10 @@ Requesting information
 
 .. cmd:: Validate Proof
 
-   This command checks that the current partial proof is well-typed.
-   It is useful to track down tactic bugs as without it errors are
-   delayed until the proof is complete.
+   Checks that the current partial proof is well-typed.
+   It is useful for finding tactic bugs since without it, such errors will only be detected at :cmd:`Qed` time.
 
-   It does not check the guard condition, use :cmd:`Guarded` for that.
+   It does not check the guard condition.  Use :cmd:`Guarded` for that.
 
 .. _showing_diffs: