Merge PR #8645: Improve markdown in changes.

8 files changed, 92 insertions, 94 deletions

diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index 4a8606a38a..73b61ee0d9 100644
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -16,4 +16,4 @@ Fixes / closes #????
 <!-- If this is a feature pull request / breaks compatibility: -->
 <!-- (Otherwise, remove these lines.) -->
 - [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
-- [ ] Entry added in CHANGES.
+- [ ] Entry added in CHANGES.md.
diff --git a/CHANGES b/CHANGES.md
index 5c664b7e2a..2f31ab1950 100644
--- a/CHANGES
+++ b/CHANGES.md
@@ -29,34 +29,34 @@ Notations
 - New support for autonomous grammars of terms, called "custom
   entries" (see chapter "Syntax extensions" of the reference manual).
 
-- New command "Declare Scope" to explicitly declare a scope name
+- New command `Declare Scope` to explicitly declare a scope name
   before any use of it. Implicit declaration of a scope at the time of
-  "Bind Scope", "Delimit Scope", "Undelimit Scope", or "Notation" is
+  `Bind Scope`, `Delimit Scope`, `Undelimit Scope`, or `Notation` is
   deprecated.
 
 Tactics
 
-- Added toplevel goal selector ! which expects a single focused goal.
-  Use with Set Default Goal Selector to force focusing before tactics
+- Added toplevel goal selector `!` which expects a single focused goal.
+  Use with `Set Default Goal Selector` to force focusing before tactics
   are called.
 
 - The undocumented "nameless" forms `fix N`, `cofix` that were
-  deprecated in 8.8 have been removed from LTAC's syntax; please use
+  deprecated in 8.8 have been removed from Ltac's syntax; please use
   `fix ident N/cofix ident` to explicitly name the (co)fixpoint
   hypothesis to be introduced.
 
-- Introduction tactics "intro"/"intros" on a goal which is an
+- Introduction tactics `intro`/`intros` on a goal that is an
   existential variable now force a refinement of the goal into a
   dependent product rather than failing.
 
-- Support for fix/cofix added in Ltac "match" and "lazymatch".
+- Support for `fix`/`cofix` added in Ltac `match` and `lazymatch`.
 
 - Ltac backtraces now include trace information about tactics
   called by OCaml-defined tactics.
 
-- Option "Ltac Debug" now applies also to terms built using Ltac functions.
+- Option `Ltac Debug` now applies also to terms built using Ltac functions.
 
-- Deprecated the Implicit Tactic family of commands.
+- Deprecated the `Implicit Tactic` family of commands.
 
 - The default program obligation tactic uses a bounded proof search
   instead of an unbounded and potentially non-terminating one now
@@ -79,7 +79,7 @@ Tactics
 - The `romega` tactics have been deprecated; please use `lia` instead.
 
 - Names of existential variables occurring in Ltac functions
-  (e.g. "?[n]" or "?n" in terms - not in patterns) are now interpreted
+  (e.g. `?[n]` or `?n` in terms - not in patterns) are now interpreted
   the same way as other variable names occurring in Ltac functions.
 
 Focusing
@@ -92,24 +92,24 @@ Specification language, type inference
 
 - A fix to unification (which was sensitive to the ascii name of
   variables) may occasionally change type inference in incompatible
-  ways, especially regarding the inference of the return clause of "match".
+  ways, especially regarding the inference of the return clause of `match`.
 
 - Fixing a missing check in interpreting instances of existential
-  variables which are bound to local definitions might exceptionally
+  variables that are bound to local definitions might exceptionally
   induce an overhead if the cost of checking the conversion of the
   corresponding definitions is additionally high (PR #8215).
 
-- A few improvements in inference of the return clause of "match" can
+- A few improvements in inference of the return clause of `match` can
   exceptionally introduce incompatibilities (PR #262). This can be
-  solved by writing an explicit "return" clause, sometimes even simply
-  an explicit "return _" clause.
+  solved by writing an explicit `return` clause, sometimes even simply
+  an explicit `return _` clause.
 
 Standard Library
 
 - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,
   and proved some lemmas about them.  Note that this might cause
-  incompatibilities if you have, e.g., string_scope and Z_scope both
-  open with string_scope on top, and expect `=?` to refer to `Z.eqb`.
+  incompatibilities if you have, e.g., `string_scope` and `Z_scope` both
+  open with `string_scope` on top, and expect `=?` to refer to `Z.eqb`.
   Solution: wrap `_ =? _` in `(_ =? _)%Z` (or whichever scope you
   want).
 
@@ -149,35 +149,34 @@ Standard Library
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
-  the command line: COQFLAGS, COQCHKFLAGS, COQDOCFLAGS.
-  COQFLAGS is now entirely separate from COQLIBS, so in custom Makefiles
-  $(COQFLAGS) should be replaced by $(COQFLAGS) $(COQLIBS).
+  the command line: `COQFLAGS`, `COQCHKFLAGS`, `COQDOCFLAGS`.
+  `COQFLAGS` is now entirely separate from `COQLIBS`, so in custom Makefiles
+  `$(COQFLAGS)` should be replaced by `$(COQFLAGS) $(COQLIBS)`.
 
-- Removed the gallina utility (extracts specification from Coq vernacular files).
+- Removed the `gallina` utility (extracts specification from Coq vernacular files).
   If you would like to maintain this tool externally, please contact us.
 
 - Removed the Emacs modes distributed with Coq. You are advised to
-  use Proof-General <https://proofgeneral.github.io/> (and optionally
-  Company-Coq <https://github.com/cpitclaudel/company-coq>) instead.
+  use [Proof-General](https://proofgeneral.github.io/) (and optionally
+  [Company-Coq](https://github.com/cpitclaudel/company-coq)) instead.
   If your use case is not covered by these alternative Emacs modes,
   please open an issue. We can help set up external maintenance as part
   of Proof-General, or independently as part of coq-community.
 
-
 Vernacular Commands
 
-- Removed deprecated commands Arguments Scope and Implicit Arguments
-  (not the option). Use the Arguments command instead.
+- Removed deprecated commands `Arguments Scope` and `Implicit Arguments`
+  (not the option). Use the `Arguments` command instead.
 - Nested proofs may be enabled through the option `Nested Proofs Allowed`.
   By default, they are disabled and produce an error. The deprecation
   warning which used to occur when using nested proofs has been removed.
-- Added option Uniform Inductive Parameters which abstracts over parameters
+- Added option `Uniform Inductive Parameters` which abstracts over parameters
   before typechecking constructors, allowing to write for example
   `Inductive list (A : Type) := nil : list | cons : A -> list -> list.`
-- New Set Hint Variables/Constants Opaque/Transparent commands for setting
+- New `Set Hint Variables/Constants Opaque/Transparent` commands for setting
   globally the opacity flag of variables and constants in hint databases,
   overwritting the opacity set of the hint database.
-- Added generic syntax for “attributes”, as in:
+- Added generic syntax for "attributes", as in:
   `#[local] Lemma foo : bar.`
 - Added the `Numeral Notation` command for registering decimal numeral
   notations for custom types
@@ -185,8 +184,8 @@ Vernacular Commands
   scope. If you want the previous behavior, use `Global Set SsrHave
   NoTCResolution`.
 - Multiple sections with the same name are allowed.
-- Combined Scheme can now work when inductive schemes are generated in sort
-  Type. It used to be limited to sort Prop.
+- `Combined Scheme` can now work when inductive schemes are generated in sort
+  `Type`. It used to be limited to sort `Prop`.
 
 Coq binaries and process model
 
@@ -204,40 +203,41 @@ SSReflect
 
 - The implementation of delayed clear switches in intro patterns
   is now simpler to explain:
-  1. The immediate effect of a clear switch like {x} is to rename the
-     variable x to _x_ (i.e. a reserved identifier that cannot be mentioned
+  1. The immediate effect of a clear switch like `{x}` is to rename the
+     variable `x` to `_x_` (i.e. a reserved identifier that cannot be mentioned
      explicitly)
-  2. The delayed effect of {x} is that _x_ is cleared at the end of the intro
+  2. The delayed effect of `{x}` is that `_x_` is cleared at the end of the intro
      pattern
-  3. A clear switch immediately before a view application like {x}/v is
-     translated to /v{x}.
-  In particular rule 3 lets one write {x}/v even if v uses the variable x:
+  3. A clear switch immediately before a view application like `{x}/v` is
+     translated to `/v{x}`.
+
+  In particular, the third rule lets one write `{x}/v` even if `v` uses the variable `x`:
   indeed the view is executed before the renaming.
 
 - An empty clear switch is now accepted in intro patterns before a
   view application whenever the view is a variable.
-  One can now write {}/v to mean {v}/v.  Remark that {}/x is very similar
-  to the idiom {}e for the rewrite tactic (the equation e is used for
+  One can now write `{}/v` to mean `{v}/v`.  Remark that `{}/x` is very similar
+  to the idiom `{}e` for the rewrite tactic (the equation `e` is used for
   rewriting and then discarded).
 
 Standard Library
 
-- There are now conversions between [string] and [positive], [Z],
-  [nat], and [N] in binary, octal, and hex.
+- There are now conversions between `string` and `positive`, `Z`,
+  `nat`, and `N` in binary, octal, and hex.
 
 Display diffs between proof steps
 
-- coqtop and coqide can now highlight the differences between proof steps
+- `coqtop` and `coqide` can now highlight the differences between proof steps
   in color. This can be enabled from the command line or the
-  `Set Diffs "on"|"off"|"removed"` command. Please see the documentation for
+  `Set Diffs "on"/"off"/"removed"` command. Please see the documentation for
   details.  Showing diffs in Proof General requires small changes to PG
   (under discussion).
 
 Notations
 
 - Added `++` infix for `VectorDef.append`.
-  Note that this might cause incompatibilities if you have, e.g., list_scope
-  and vector_scope both open with vector_scope on top, and expect `++` to
+  Note that this might cause incompatibilities if you have, e.g., `list_scope`
+  and `vector_scope` both open with `vector_scope` on top, and expect `++` to
   refer to `app`.
   Solution: wrap `_ ++ _` in `(_ ++ _)%list` (or whichever scope you want).
 
@@ -263,7 +263,7 @@ Kernel
 Windows installer
 
 - The Windows installer now includes many more external packages that can be
-individually selected for installation.
+  individually selected for installation.
 
 Many other bug fixes and lots of documentation improvements (for details,
 see the 8.8.2 milestone at https://github.com/coq/coq/milestone/15?closed=1).
@@ -273,10 +273,10 @@ Changes from 8.8.0 to 8.8.1
 
 Kernel
 
-- Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333).
+- Fix a critical bug with cofixpoints and `vm_compute`/`native_compute` (#7333).
 - Fix a critical bug with modules and algebraic universes (#7695)
 - Fix a critical bug with inlining of polymorphic constants (#7615).
-- Fix a critical bug with universe polymorphism and vm_compute (#7723). Was
+- Fix a critical bug with universe polymorphism and `vm_compute` (#7723). Was
   present since 8.5.
 
 Notations
@@ -300,7 +300,7 @@ Changes from 8.8+beta1 to 8.8.0
 Tools
 
 - Asynchronous proof delegation policy was fixed. Since version 8.7
-  Coq was ignoring previous runs and the -async-proofs-delegation-threshold
+  Coq was ignoring previous runs and the `-async-proofs-delegation-threshold`
   option did not have the expected behavior.
 
 Tactic language
diff --git a/README.md b/README.md
index fcf20f0097..e6a52e95e3 100644
--- a/README.md
+++ b/README.md
@@ -27,7 +27,7 @@ and the [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ),
 for additional user-contributed documentation.
 
 ## Changes
-There is a file named [`CHANGES`](CHANGES) that explains the differences and the
+There is a file named [`CHANGES.md`](CHANGES.md) that explains the differences and the
 incompatibilities since last versions. If you upgrade Coq, please read
 it carefully.
 
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 5f07aa8fca..b8bea755e0 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1374,7 +1374,7 @@ function copy_coq_license {
     # FIXME: this is not the micromega license
     # It only applies to code that was copied into one single file!
     install -D README.md                      "$PREFIXCOQ/license_readme/coq/ReadMe.md"
-    install -D CHANGES                        "$PREFIXCOQ/license_readme/coq/Changes.txt"
+    install -D CHANGES.md                     "$PREFIXCOQ/license_readme/coq/Changes.md"
     install -D INSTALL                        "$PREFIXCOQ/license_readme/coq/Install.txt"
     install -D doc/README.md                  "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
   fi
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 24952eb5b7..7870cbb51d 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -126,7 +126,7 @@ patch (or ask someone to prepare a patch) to fix the project:
    developer who merges the PR on Coq. There are plans to improve this, cf.
    [#6724](https://github.com/coq/coq/issues/6724).
 
-Moreover your PR must absolutely update the [`CHANGES`](../../CHANGES) file.
+Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file.
 
 Advanced GitLab CI information
 ------------------------------
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index c0cd9c8cdd..000f21c254 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -54,7 +54,7 @@ those external projects should have been prepared (cf. the relevant sub-section
 in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested
 with these fixes thanks to ["overlays"](../ci/user-overlays/README.md).
 
-Moreover the PR must absolutely update the [`CHANGES`](../../CHANGES) file.
+Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file.
 
 If overlays are missing, ask the author to prepare them and label the PR with
 the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
@@ -93,7 +93,7 @@ When the PR has conflicts, the assignee can either:
 
 In both cases, CI should be run again.
 
-In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix
+In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix
 the conflicts in the merge commit (following the same steps as below), and push
 to `master` directly. Don't use the GitHub interface to fix these conflicts.
 
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index fdeb0abed4..9d592ee879 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,12 +1,5 @@
 ## Changes between Coq 8.9 and Coq 8.10
 
-### ML API
-
-Termops:
-
-- Internal printing functions have been placed under the
-  `Termops.Internal` namespace.
-
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
@@ -16,8 +9,8 @@ Names
 - In `Libnames`, the type `reference` and its two constructors `Qualid` and
   `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity,
   `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be
-  replaced by a test using `qualid_is_ident`. Extracting the ident part of a
-  qualid can be done using `qualid_basename`.
+  replaced by a test using `qualid_is_ident`. Extracting the `ident` part of a
+  `qualid` can be done using `qualid_basename`.
 
 Misctypes
 
@@ -51,20 +44,20 @@ Proof engine
 
 ML Libraries used by Coq
 
-- Introduction of a "Smart" module for collecting "smart*" functions, e.g.
-  Array.Smart.map.
-- Uniformization of some names, e.g. Array.Smart.fold_left_map instead
-  of Array.smartfoldmap.
+- Introduction of a `Smart` module for collecting `smart*` functions, e.g.
+  `Array.Smart.map`.
+- Uniformization of some names, e.g. `Array.Smart.fold_left_map` instead
+  of `Array.smartfoldmap`.
 
 Printer.ml API
 
-- The mechanism in Printer that allowed dynamically overriding pr_subgoals,
-  pr_subgoal and pr_goal was removed to simplify the code.  It was
-  earlierly used by PCoq.
+- The mechanism in `Printer` that allowed dynamically overriding `pr_subgoals`,
+  `pr_subgoal` and `pr_goal` was removed to simplify the code.  It was
+  earlier used by PCoq.
 
 Kernel
 
-  The following renamings happened:
+- The following renamings happened:
   - `Context.Rel.t` into `Constr.rel_context`
   - `Context.Named.t` into `Constr.named_context`
   - `Context.Compacted.t` into `Constr.compacted_context`
@@ -93,19 +86,24 @@ Vernacular commands
 
 Primitive number parsers
 
-- For better modularity, the primitive parsers for positive, N and Z
-  have been split over three files (plugins/syntax/positive_syntax.ml,
-  plugins/syntax/n_syntax.ml, plugins/syntax/z_syntax.ml).
+- For better modularity, the primitive parsers for `positive`, `N` and `Z`
+  have been split over three files (`plugins/syntax/positive_syntax.ml`,
+  `plugins/syntax/n_syntax.ml`, `plugins/syntax/z_syntax.ml`).
 
 Parsing
 
-- Manual uses of the Pcoq.Gram module have been deprecated. Wrapper modules
-  Pcoq.Entry and Pcoq.Parsable were introduced to replace it.
+- Manual uses of the `Pcoq.Gram` module have been deprecated. Wrapper modules
+  `Pcoq.Entry` and `Pcoq.Parsable` were introduced to replace it.
+
+Termops
+
+- Internal printing functions have been placed under the
+  `Termops.Internal` namespace.
 
 ### Unit testing
 
-  The test suite now allows writing unit tests against OCaml code in the Coq
-  code base. Those unit tests create a dependency on the OUnit test framework.
+The test suite now allows writing unit tests against OCaml code in the Coq
+code base. Those unit tests create a dependency on the OUnit test framework.
 
 ### Transitioning away from Camlp5
 
@@ -140,7 +138,7 @@ let myval = 0
 
 Steps to perform:
 - replace the brackets enclosing OCaml code in actions with braces
-- if not there yet, add a leading `|̀  to the first rule
+- if not there yet, add a leading `|` to the first rule
 
 For instance, code of the form:
 ```
@@ -171,8 +169,8 @@ Most plugin writers do not need this low-level interface, but for the sake of
 completeness we document it.
 
 Steps to perform are:
-- replace GEXTEND with GRAMMAR EXTEND
-- wrap every occurrence of OCaml code in actions into braces { }
+- replace `GEXTEND` with `GRAMMAR EXTEND`
+- wrap every occurrence of OCaml code in actions into braces `{ }`
 
 For instance, code of the form
 ```
@@ -222,7 +220,7 @@ All the other bugs kept their number.
 
 General deprecation
 
-- All functions marked [@@ocaml.deprecated] in 8.7 have been
+- All functions marked `[@@ocaml.deprecated]` in 8.7 have been
   removed. Please, make sure your plugin is warning-free in 8.7 before
   trying to port it over 8.8.
 
@@ -250,8 +248,8 @@ We changed the type of the following functions:
 
 - `Global.body_of_constant`: same as above.
 
-- `Constrinterp.*` generally, many functions that used to take an
-  `evar_map ref` have been now switched to functions that will work in
+- `Constrinterp.*`: generally, many functions that used to take an
+  `evar_map ref` have now been switched to functions that will work in
   a functional way. The old style of passing `evar_map`s as references
   is not supported anymore.
 
@@ -269,16 +267,16 @@ We have changed the representation of the following types:
 
 Some tactics and related functions now support static configurability, e.g.:
 
-- injectable, dEq, etc. takes an argument ~keep_proofs which,
-  - if None, tells to behave as told with the flag Keep Proof Equalities
-  - if Some b, tells to keep proof equalities iff b is true
+- `injectable`, `dEq`, etc. take an argument `~keep_proofs` which,
+  - if `None`, tells to behave as told with the flag `Keep Proof Equalities`
+  - if `Some b`, tells to keep proof equalities iff `b` is true
 
 Declaration of printers for arguments used only in vernac command
 
-- It should now use "declare_extra_vernac_genarg_pprule" rather than
-  "declare_extra_genarg_pprule", otherwise, a failure at runtime might
+- It should now use `declare_extra_vernac_genarg_pprule` rather than
+  `declare_extra_genarg_pprule`, otherwise, a failure at runtime might
   happen. An alternative is to register the corresponding argument as
-  a value, using "Geninterp.register_val0 wit None".
+  a value, using `Geninterp.register_val0 wit None`.
 
 Types Alias deprecation and type relocation.
 
@@ -321,7 +319,7 @@ functions when some given constants are traversed:
 
   * `declare_reduction_effect`: to declare a hook to be applied when some
   constant are visited during the execution of some reduction functions
-  (primarily cbv).
+  (primarily `cbv`).
 
   * `set_reduction_effect`: to declare a constant on which a given effect
   hook should be called.
diff --git a/doc/sphinx/credits-contents.rst b/doc/sphinx/credits-contents.rst
index 212f0a65b0..d1df0657aa 100644
--- a/doc/sphinx/credits-contents.rst
+++ b/doc/sphinx/credits-contents.rst
@@ -1238,7 +1238,7 @@ of integers and real constants are now represented using `IZR` (work by
 Guillaume Melquiond).
 
 Standard library additions and improvements by Jason Gross, Pierre Letouzey and
-others, documented in the `CHANGES` file.
+others, documented in the ``CHANGES.md`` file.
 
 The mathematical proof language/declarative mode plugin was removed from the
 archive.
@@ -1352,7 +1352,7 @@ version.
 
 Version 8.8 also comes with a bunch of smaller-scale changes and
 improvements regarding the different components of the system.
-Most important ones are documented in the ``CHANGES`` file.
+Most important ones are documented in the ``CHANGES.md`` file.
 
 The efficiency of the whole system has seen improvements thanks to
 contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, Maxime Dénès and