11 files changed, 89 insertions, 32 deletions
diff --git a/doc/changelog/02-specification-language/10331-minim-prop-toset.rst b/doc/changelog/02-specification-language/10331-minim-prop-toset.rst
new file mode 100644
index 0000000000..6c442ca1aa
--- /dev/null
+++ b/doc/changelog/02-specification-language/10331-minim-prop-toset.rst
@@ -0,0 +1,5 @@
+- **Changed:** Heuristics for universe minimization to :g:`Set`: also
+  use constraints ``Prop <= i`` (`#10331
+  <https://github.com/coq/coq/pull/10331>`_, by Gaëtan Gilbert with
+  help from Maxime Dénès and Matthieu Sozeau, fixes `#12414
+  <https://github.com/coq/coq/issues/12414>`_).
diff --git a/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst b/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst
new file mode 100644
index 0000000000..16fc91f911
--- /dev/null
+++ b/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst
@@ -0,0 +1,10 @@
+- **Changed:**
+  New model for ``only parsing`` and ``only printing`` notations with
+  support for at most one parsing-and-printing or only-parsing
+  notation per notation and scope, but an arbitrary number of
+  only-printing notations
+  (`#12950 <https://github.com/coq/coq/pull/12950>`_,
+  fixes `#4738 <https://github.com/coq/coq/issues/4738>`_
+  and `#9682 <https://github.com/coq/coq/issues/9682>`_
+  and part 2 of `#12908 <https://github.com/coq/coq/issues/12908>`_,
+  by Hugo Herbelin).
diff --git a/doc/changelog/09-coqide/12874-show_proof_diffs.rst b/doc/changelog/09-coqide/12874-show_proof_diffs.rst
new file mode 100644
index 0000000000..51bebad9be
--- /dev/null
+++ b/doc/changelog/09-coqide/12874-show_proof_diffs.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Support showing diffs for :cmd:`Show Proof` in CoqIDE from the :n:`View` menu.
+  See :ref:`showing_proof_diffs`.
+  (`#12874 <https://github.com/coq/coq/pull/12874>`_,
+  by Jim Fehrle and Enrico Tassi)
diff --git a/doc/sphinx/_static/diffs-show-proof.png b/doc/sphinx/_static/diffs-show-proof.png
new file mode 100644
index 0000000000..62bd9cccd0
--- /dev/null
+++ b/doc/sphinx/_static/diffs-show-proof.png
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 4cdfba146a..39b154de8d 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -13,7 +13,7 @@ Inductive types
    .. prodn::
       inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
       constructors_or_record ::= {? %| } {+| @constructor }
-      | {? @ident } %{ {*; @record_field } %}
+      | {? @ident } %{ {*; @record_field } {? ; } %}
       constructor ::= @ident {* @binder } {? @of_type }
 
    This command defines one or more
diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index cd44d06e67..b2099b8636 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -18,12 +18,12 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
    .. insertprodn record_definition field_def
 
    .. prodn::
-      record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations }
+      record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } {? ; } %} {? @decl_notations }
       record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations }
       field_body ::= {* @binder } @of_type
       | {* @binder } @of_type := @term
       | {* @binder } := @term
-      term_record ::= %{%| {* @field_def } %|%}
+      term_record ::= %{%| {*; @field_def } {? ; } %|%}
       field_def ::= @qualid {* @binder } := @term
 
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index f90ebadb3a..f722ddda79 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -590,11 +590,11 @@ Requesting information
       constructed. Each hole is an existential variable, which appears as a
       question mark followed by an identifier.
 
-      Experimental: Specifying “Diffs” highlights the difference between the
+      Specifying “Diffs” highlights the difference between the
       current and previous proof step.  By default, the command shows the
       output once with additions highlighted.  Including “removed” shows
       the output twice: once showing removals and once showing additions.
-      It does not examine the :opt:`Diffs` option.  See :ref:`showing_diffs`.
+      It does not examine the :opt:`Diffs` option.  See :ref:`showing_proof_diffs`.
 
    .. cmdv:: Show Conjectures
       :name: Show Conjectures
@@ -675,12 +675,9 @@ Requesting information
 Showing differences between proof steps
 ---------------------------------------
 
-
 Coq can automatically highlight the differences between successive proof steps
-and between values in some error messages.  Also, as an experimental feature,
-Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof`
-command, but only, for now, when using coqtop and Proof General.
-
+and between values in some error messages.  Coq can also highlight differences
+in the proof term.
 For example, the following screenshots of CoqIDE and coqtop show the application
 of the same :tacn:`intros` tactic.  The tactic creates two new hypotheses, highlighted in green.
 The conclusion is entirely in pale green because although it’s changed, no tokens were added
@@ -826,14 +823,37 @@ the split because it has not changed.
   .. image:: ../_static/diffs-coqide-multigoal.png
      :alt: coqide with Set Diffs on with multiple goals
 
-This is how diffs may appear after applying a :tacn:`intro` tactic that results
-in compacted hypotheses:
+Diffs may appear like this after applying a :tacn:`intro` tactic that results
+in a compacted hypotheses:
 
 ..
 
   .. image:: ../_static/diffs-coqide-compacted.png
      :alt: coqide with Set Diffs on with compacted hypotheses
 
+.. _showing_proof_diffs:
+
+"Show Proof" differences
+````````````````````````
+
+To show differences in the proof term:
+
+- In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command.
+
+- In CoqIDE, position the cursor on or just after a tactic to compare the proof term
+  after the tactic with the proof term before the tactic, then select
+  `View / Show Proof` from the menu or enter the associated key binding.
+  Differences will be shown applying the current `Show Diffs` setting
+  from the `View` menu.  If the current setting is `Don't show diffs`, diffs
+  will not be shown.
+
+  Output with the "added and removed" option looks like this:
+
+  ..
+
+    .. image:: ../_static/diffs-show-proof.png
+       :alt: coqide with Set Diffs on with compacted hypotheses
+
 Controlling the effect of proof editing commands
 ------------------------------------------------
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 5148fa84c9..d6db305300 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -57,15 +57,14 @@ to represent :g:`(and A B)`:
 Notations must be in double quotes, except when the
 abbreviation has the form of an ordinary applicative expression;
 see :ref:`Abbreviations`. The notation consists of *tokens* separated by
-spaces. Alphanumeric strings (such as ``A`` and ``B``) are the *parameters*
+spaces. Tokens which are identifiers (such as ``A``, ``x0'``, etc.) are the *parameters*
 of the notation. Each of them must occur at least once in the abbreviated term. The
 other elements of the string (such as ``/\``) are the *symbols*.
 
-Substrings enclosed in single quotes are treated as literals.  This is necessary
-for substrings that would otherwise be interpreted as :n:`@ident`\s.  Similarly,
-every symbol of at least 3 characters and starting with a simple quote
-must be quoted (then it starts by two single quotes). Here is an
-example.
+Identifiers enclosed in single quotes are treated as symbols and thus
+lose their role of parameters. In the same vein, every symbol of at
+least 3 characters and starting with a simple quote must be quoted
+(then it starts with two single quotes). Here is an example.
 
 .. coqtop:: in
 
@@ -82,7 +81,8 @@ associativity rules have to be given.
    The right-hand side of a notation is interpreted at the time the notation is
    given. In particular, disambiguation of constants, :ref:`implicit arguments
    <ImplicitArguments>` and other notations are resolved at the
-   time of the declaration of the notation.
+   time of the declaration of the notation. The right-hand side is
+   currently typed only at use time but this may change in the future.
 
 Precedences and associativity
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -299,12 +299,29 @@ Notations disappear when a section is closed. No typing of the denoted
 expression is performed at definition time. Type checking is done only
 at the time of use of the notation.
 
-.. note:: Sometimes, a notation is expected only for the parser. To do
-          so, the option ``only parsing`` is allowed in the list of :n:`@syntax_modifier`\s
-          in :cmd:`Notation`. Conversely, the ``only printing`` :n:`@syntax_modifier` can be
-          used to declare that a notation should only be used for printing and
-          should not declare a parsing rule. In particular, such notations do
-          not modify the parser.
+.. note::
+
+   The default for a notation is to be used both for parsing and
+   printing. It is possible to declare a notation only for parsing by
+   adding the option ``only parsing`` to the list of
+   :n:`@syntax_modifier`\s of :cmd:`Notation`. Symmetrically, the
+   ``only printing`` :n:`@syntax_modifier` can be used to declare that
+   a notation should only be used for printing.
+
+   If a notation to be used both for parsing and printing is
+   overriden, both the parsing and printing are invalided, even if the
+   overriding rule is only parsing.
+
+   If a given notation string occurs only in ``only printing`` rules,
+   the parser is not modified at all.
+
+   To a given notation string and scope can be attached at most one
+   notation with both parsing and printing or with only
+   parsing. Contrastingly, an arbitrary number of ``only printing``
+   notations differing in their right-hand sides but only a unique
+   right-hand side can be attached to a given string and
+   scope. Obviously, expressions printed by means of such extra
+   printing rules will not be reparsed to the same form.
 
 The Infix command
 ~~~~~~~~~~~~~~~~~~
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a9f9c805d8..1e9be8dded 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -396,8 +396,8 @@ operconstr0: [
 (* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *)
 | DELETE "{" binder_constr "}"
 | REPLACE "{|" record_declaration bar_cbrace
-| WITH "{|" LIST0 field_def bar_cbrace
-| MOVETO term_record "{|" LIST0 field_def bar_cbrace
+| WITH "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
+| MOVETO term_record "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
 | MOVETO term_generalizing "`{" operconstr200 "}"
 | MOVETO term_generalizing "`(" operconstr200 ")"
 | MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")"
@@ -585,7 +585,7 @@ constructor_list_or_record_decl: [
 
 record_fields: [
 | REPLACE record_field ";" record_fields
-| WITH LIST0 record_field SEP ";"
+| WITH LIST0 record_field SEP ";" OPT ";"
 | DELETE record_field
 | DELETE (* empty *)
 ]
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 067050b4f5..73641976e3 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1740,11 +1740,11 @@ simple_tactic: [
 | "zify_elim_let"      (* micromega plugin *)
 | "nsatz_compute" constr      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
-| "rtauto"
 | "protect_fv" string "in" ident      (* ring plugin *)
 | "protect_fv" string      (* ring plugin *)
 | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr      (* ring plugin *)
 | "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr      (* ring plugin *)
+| "rtauto"
 ]
 
 mlname: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index cbef29fb39..61befe9f1f 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -539,7 +539,7 @@ variant_definition: [
 ]
 
 record_definition: [
-| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" "}" OPT decl_notations
+| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}" OPT decl_notations
 ]
 
 record_field: [
@@ -553,7 +553,7 @@ field_body: [
 ]
 
 term_record: [
-| "{|" LIST0 field_def "|}"
+| "{|" LIST0 field_def SEP ";" OPT ";" "|}"
 ]
 
 field_def: [
@@ -566,7 +566,7 @@ inductive_definition: [
 
 constructors_or_record: [
 | OPT "|" LIST1 constructor SEP "|"
-| OPT ident "{" LIST0 record_field SEP ";" "}"
+| OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}"
 ]
 
 constructor: [