Add more documentation to CoqMakefile.local-late

As requested in PR comments

Change passive voice to active voice and fix a grammar error
As per coq#12411 (comment)

Add more documentation about Makefile var use

Also apply suggestions from code review

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

doc/changelog/08-tools/12411-makefile-local-late.rst

@@ -1,5 +1,5 @@
 - **Added:**
   ``coq_makefile``\-made ``Makefile``\s now support inclusion of a
-  ``.local-late`` file at the very end, in case the user wants to have access
-  to more variables (`#12411 <https://github.com/coq/coq/pull/12411>`_, fixes
+  ``.local-late`` file at the end, allowing the user to access
+  more variables (`#12411 <https://github.com/coq/coq/pull/12411>`_, fixes
   `#10912 <https://github.com/coq/coq/issues/10912>`_, by Jason Gross).

doc/sphinx/practical-tools/utilities.rst

@@ -152,16 +152,27 @@ Including the generated makefile with an include directive is
 discouraged, since the contents of this file, including variable names and
 status of rules, may change in the future.
 
-An optional file ``CoqMakefile.local`` can be provided by the user in order to
-extend ``CoqMakefile``. In particular one can declare custom actions to be
-performed before or after the build process. Similarly one can customize the
-install target or even provide new targets. Extension points are documented in
-paragraph :ref:`coqmakefilelocal`. If the user needs to access variables
-defined in the ``Makefile``, the optional file ``CoqMakefile.local-late`` can
-be used.
-
-The extensions of the files listed in ``_CoqProject`` is used in order to
-decide how to build them. In particular:
+Use the optional file ``CoqMakefile.local`` to extend
+``CoqMakefile``. In particular, you can declare custom actions to run
+before or after the build process. Similarly you can customize the
+install target or even provide new targets. See
+:ref:`coqmakefilelocal` for extension-point documentation. Although
+you can use all variables defined in ``CoqMakefile`` in the *recipes*
+of rules that you write and in the definitions of any variables that
+you assign with ``=``, many variables are not available for use if you
+assign variable values with ``:=`` nor to define the *targets* of
+rules nor in top-level conditionals such as ``ifeq``. Additionally,
+you must use `secondary expansion
+<https://www.gnu.org/software/make/manual/html_node/Secondary-Expansion.html>`_
+to make use of such variables in the prerequisites of rules. To access
+variables defined in ``CoqMakefile`` in rule target computation,
+top-level conditionals, and ``:=`` variable assignment, for example to
+add new dependencies to compiled outputs, use the optional file
+``CoqMakefile.local-late``.  See :ref:`coqmakefilelocallate` for a
+non-exhaustive list of variables.
+
+The extensions of files listed in ``_CoqProject`` determine
+how they are built. In particular:
 
 
 + Coq files must use the ``.v`` extension
@@ -190,9 +201,8 @@ file ``CoqMakefile``. It can contain two kinds of directives.
 **Variable assignment**
 
 The variable must belong to the variables listed in the ``Parameters``
-section of the generated makefile.  If access to more variables are
-needed, ``CoqMakefile.local-late`` can be used instead. Here we
-describe only few of the variables.
+section of the generated makefile.  Use
+``CoqMakefile.local-late`` instead to access more variables. These include:
 
 :CAMLPKGS:
    can be used to specify third party findlib packages, and is
@@ -276,6 +286,40 @@ The following makefile rules can be extended.
   One can append lines to the generated ``.merlin`` file extending this
   target.
 
+.. _coqmakefilelocallate:
+
+CoqMakefile.local-late
+++++++++++++++++++++++
+
+The optional file ``CoqMakefile.local-late`` is included at the end of the generated
+file ``CoqMakefile``.  The following is a partial list of accessible variables:
+
+:COQ_VERSION:
+   the version of ``coqc`` being used, which can be used to
+   provide different behavior depending on the Coq version
+:COQMAKEFILE_VERSION:
+   the version of Coq used to generate the
+   Makefile, which can be used to detect version mismatches
+:ALLDFILES:
+   the list of generated dependency files, which can be used,
+   for example, to cause ``make`` to recompute dependencies
+   when files change by writing ``$(ALLDFILES): myfiles`` or to
+   indicate that files must be generated before dependencies can
+   be computed by writing ``$(ALLDFILES): | mygeneratedfiles``
+:VOFILES, GLOBFILES, CMOFILES, CMXFILES, OFILES, CMAFILES, CMXAFILES, CMIFILES, CMXSFILES:
+   lists of files that are generated by various invocations of the compilers
+
+In addition, the following variables may be useful for
+deciding what targets to present via ``$(shell ...)``; these
+variables are already accessible in recipes for rules added in
+``CoqMakefile.local``, but are only accessible from top-level ``$(shell
+...)`` invocations in ``CoqMakefile.local-late``:
+
+:COQC, COQDEP, COQDOC, CAMLC, CAMLOPTC:
+   compiler binaries
+:COQFLAGS, CAMLFLAGS, COQLIBS, COQDEBUG, OCAMLLIBS:
+   flags passed to the Coq or OCaml compilers
+
 Timing targets and performance testing
 ++++++++++++++++++++++++++++++++++++++
 

tools/CoqMakefile.in

@@ -913,8 +913,8 @@ debug:
 
 .DEFAULT_GOAL := all
 
-# This file can be created by the user to hook into double colon rules
-# or add any other Makefile code he may need, making use of defined
+# Users can create @LOCAL_LATE_FILE@ to hook into double-colon rules
+# or add other needed Makefile code, using defined
 # variables if necessary.
 -include @LOCAL_LATE_FILE@