Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into multiple pages.

Reviewed-by: jfehrle

3 files changed, 67 insertions, 3 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 90173d65bf..a21f7e545c 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -28,9 +28,8 @@ especially about its foundations, please refer to :cite:`Del00`.
 Syntax
 ------
 
-The syntax of the tactic language is given below. See Chapter
-:ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used
-in these grammar rules. Various already defined entries will be used in this
+The syntax of the tactic language is given below.
+Various already defined entries will be used in this
 chapter: entries :token:`num`, :token:`int`, :token:`ident`
 :token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic`
 represent respectively natural and integer numbers,
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index ad799fbbcd..3fec940fad 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2977,6 +2977,41 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 Performing computations
 ---------------------------
 
+.. insertprodn red_expr pattern_occ
+
+.. prodn::
+   red_expr ::= red
+   | hnf
+   | simpl {? @delta_flag } {? @ref_or_pattern_occ }
+   | cbv {? @strategy_flag }
+   | cbn {? @strategy_flag }
+   | lazy {? @strategy_flag }
+   | compute {? @delta_flag }
+   | vm_compute {? @ref_or_pattern_occ }
+   | native_compute {? @ref_or_pattern_occ }
+   | unfold {+, @unfold_occ }
+   | fold {+ @one_term }
+   | pattern {+, @pattern_occ }
+   | @ident
+   delta_flag ::= {? - } [ {+ @smart_qualid } ]
+   strategy_flag ::= {+ @red_flags }
+   | @delta_flag
+   red_flags ::= beta
+   | iota
+   | match
+   | fix
+   | cofix
+   | zeta
+   | delta {? @delta_flag }
+   ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums }
+   | @one_term {? at @occs_nums }
+   occs_nums ::= {+ {| @num | @ident } }
+   | - {| @num | @ident } {* @int_or_var }
+   int_or_var ::= @int
+   | @ident
+   unfold_occ ::= @smart_qualid {? at @occs_nums }
+   pattern_occ ::= @one_term {? at @occs_nums }
+
 This set of tactics implements different specialized usages of the
 tactic :tacn:`change`.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7191444bac..031abbe15c 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -747,6 +747,36 @@ Controlling display
    after each tactic.  The information is used by the Prooftree tool in Proof
    General. (https://askra.de/software/prooftree)
 
+.. extracted from Gallina extensions chapter
+
+.. _printing_constructions_full:
+
+Printing constructions in full
+------------------------------
+
+.. flag:: Printing All
+
+   Coercions, implicit arguments, the type of pattern matching, but also
+   notations (see :ref:`syntax-extensions-and-notation-scopes`) can obfuscate the behavior of some
+   tactics (typically the tactics applying to occurrences of subterms are
+   sensitive to the implicit arguments). Turning this flag on
+   deactivates all high-level printing features such as coercions,
+   implicit arguments, returned type of pattern matching, notations and
+   various syntactic sugar for pattern matching or record projections.
+   Otherwise said, :flag:`Printing All` includes the effects of the flags
+   :flag:`Printing Implicit`, :flag:`Printing Coercions`, :flag:`Printing Synth`,
+   :flag:`Printing Projections`, and :flag:`Printing Notations`. To reactivate
+   the high-level printing features, use the command ``Unset Printing All``.
+
+   .. note:: In some cases, setting :flag:`Printing All` may display terms
+      that are so big they become very hard to read.  One technique to work around
+      this is use :cmd:`Undelimit Scope` and/or :cmd:`Close Scope` to turn off the
+      printing of notations bound to particular scope(s).  This can be useful when
+      notations in a given scope are getting in the way of understanding
+      a goal, but turning off all notations with :flag:`Printing All` would make
+      the goal unreadable.
+
+      .. see a contrived example here: https://github.com/coq/coq/pull/11718#discussion_r415481854
 
 .. _vernac-controlling-the-reduction-strategies: