Move essential vocabulary and syntax conventions to section on basics.

3 files changed, 328 insertions, 63 deletions

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 03da59e0bf..9473cc5a15 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -1,7 +1,84 @@
+=============================
+Basic notions and conventions
+=============================
+
+This section provides some essential notions and conventions for reading
+the manual.
+
+We start by explaining the syntax and lexical conventions used in the
+manual.  Then, we present the essential vocabulary necessary to read
+the rest of the manual.  Other terms are defined throughout the manual.
+The reader may refer to the :ref:`glossary index <glossary_index>`
+for a complete list of defined terms.  Finally, we describe the various types of
+settings that |Coq| provides.
+
+Syntax and lexical conventions
+------------------------------
+
+Syntax conventions
+~~~~~~~~~~~~~~~~~~
+
+The syntax described in this documentation is equivalent to that
+accepted by the |Coq| parser, but the grammar has been edited
+to improve readability and presentation.
+
+In the grammar presented in this manual, the terminal symbols are
+black (e.g. :n:`forall`), whereas the nonterminals are green, italic
+and hyperlinked (e.g. :n:`@term`).  Some syntax is represented
+graphically using the following kinds of blocks:
+
+:n:`{? item }`
+   An optional item.
+
+:n:`{+ item }`
+   A list of one or more items.
+
+:n:`{* item }`
+   An optional list of items.
+
+:n:`{+s item}`
+   A list of one or more items separated by "s" (e.g. :n:`item__1 s item__2 s item__3`).
+
+:n:`{*s item}`
+   An optional list of items separated by "s".
+
+:n:`{| item__1 | item__2 | ... }`
+   Alternatives (either :n:`item__1` or :n:`item__2` or ...).
+
+`Precedence levels
+<https://en.wikipedia.org/wiki/Order_of_operations>`_ that are
+implemented in the |Coq| parser are shown in the documentation by
+appending the level to the nonterminal name (as in :n:`@term100` or
+:n:`@ltac_expr3`).
+
+.. note::
+
+   |Coq| uses an extensible parser.  Plugins and the :ref:`notation
+   system <syntax-extensions-and-notation-scopes>` can extend the
+   syntax at run time.  Some notations are defined in the prelude,
+   which is loaded by default.  The documented grammar doesn't include
+   these notations.  Precedence levels not used by the base grammar
+   are omitted from the documentation, even though they could still be
+   populated by notations or plugins.
+
+   Furthermore, some parsing rules are only activated in certain
+   contexts (:ref:`interactive proof mode <proofhandling>`,
+   :ref:`custom entries <custom-entries>`...).
+
+.. warning::
+
+   Given the complexity of these parsing rules, it would be extremely
+   difficult to create an external program that can properly parse a
+   |Coq| document.  Therefore, tool writers are advised to delegate
+   parsing to |Coq|, by communicating with it, for instance through
+   `SerAPI <https://github.com/ejgallego/coq-serapi>`_.
+
+.. seealso:: :cmd:`Print Grammar`
+
 .. _lexical-conventions:
 
 Lexical conventions
-===================
+~~~~~~~~~~~~~~~~~~~
 
 Blanks
   Space, newline and horizontal tab are considered blanks.
@@ -56,24 +133,22 @@ Keywords
   The following character sequences are reserved keywords that cannot be
   used as identifiers::
 
-    _ Axiom CoFixpoint Definition Fixpoint Hypothesis IF Parameter Prop
-    SProp Set Theorem Type Variable as at by cofix discriminated else
-    end exists exists2 fix for forall fun if in lazymatch let match
-    multimatch return then using where with
+    _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop
+    SProp Set Theorem Type Variable as at cofix discriminated else end
+    fix for forall fun if in let match return then where with
 
-  Note that plugins may define additional keywords when they are loaded.
+  Note that notations and plugins may define additional keywords.
 
 Other tokens
   The set of
   tokens defined at any given time can vary because the :cmd:`Notation`
   command can define new tokens.  A :cmd:`Require` command may load more notation definitions,
   while the end of a :cmd:`Section` may remove notations.  Some notations
-  are defined in the basic library (see :ref:`thecoqlibrary`) and are normally
+  are defined in the standard library (see :ref:`thecoqlibrary`) and are generally
   loaded automatically at startup time.
 
-  Here are the character sequences that Coq directly defines as tokens
-  without using :cmd:`Notation` (omitting 25 specialized tokens that begin with
-  ``#int63_``)::
+  Here are the character sequences that |Coq| directly defines as tokens
+  without using :cmd:`Notation`::
 
     ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - ->
     . .( .. ... / : ::= := :> :>> ; < <+ <- <:
@@ -87,28 +162,190 @@ Other tokens
   ``~~`` generate different tokens, whereas if `~~` is not defined, then the
   two inputs are equivalent.
 
-.. _gallina-attributes:
+Essential vocabulary
+--------------------
+
+This section presents the most essential notions to understand the
+rest of the |Coq| manual: :term:`terms <term>` and :term:`types
+<type>` on the one hand, :term:`commands <command>` and :term:`tactics
+<tactic>` on the other hand.
+
+.. glossary::
+
+   term
+
+     Terms are the basic expressions of |Coq|.  Terms can represent
+     mathematical expressions, propositions and proofs, but also
+     executable programs and program types.
+
+     Here is the top-level syntax of terms.  Each of the listed
+     constructs is presented in a dedicated section.  Some of these
+     constructs (like :n:`@term_forall_or_fun`) are part of the core
+     language that the kernel of |Coq| understands and are therefore
+     described in :ref:`this chapter <core-language>`, while
+     others (like :n:`@term_if`) are language extensions that are
+     presented in :ref:`the next chapter <extensions>`.
+
+     .. insertprodn term qualid_annotated
+
+     .. prodn::
+        term ::= @term_forall_or_fun
+        | @term_let
+        | @term_if
+        | @term_fix
+        | @term_cofix
+        | @term100
+        term100 ::= @term_cast
+        | @term10
+        term10 ::= @term_application
+        | @one_term
+        one_term ::= @term_explicit
+        | @term1
+        term1 ::= @term_projection
+        | @term_scope
+        | @term0
+        term0 ::= @qualid_annotated
+        | @sort
+        | @primitive_notations
+        | @term_evar
+        | @term_match
+        | @term_record
+        | @term_generalizing
+        | @term_ltac
+        | ( @term )
+        qualid_annotated ::= @qualid {? @univ_annot }
+
+     .. note::
+
+        Many :term:`commands <command>` and :term:`tactics <tactic>`
+        use :n:`@one_term` (in the syntax of their arguments) rather
+        than :n:`@term`.  The former need to be enclosed in
+        parentheses unless they're very simple, such as a single
+        identifier.  This avoids confusing a space-separated list of
+        terms or identifiers with a :n:`@term_application`.
+
+   type
+
+     To be valid and accepted by the |Coq| kernel, a term needs an
+     associated type.  We express this relationship by “:math:`x` *of
+     type* :math:`T`”, which we write as “:math:`x:T`”.  Informally,
+     “:math:`x:T`” can be thought as “:math:`x` *belongs to*
+     :math:`T`”.
+
+     The |Coq| kernel is a type checker: it verifies that a term has
+     the expected type by applying a set of typing rules (see
+     :ref:`Typing-rules`).  If that's indeed the case, we say that the
+     term is :gdef:`well-typed`.
+
+     A special feature of the |Coq| language is that types can depend
+     on terms (we say that the language is `dependently-typed
+     <https://en.wikipedia.org/wiki/Dependent_type>`_).  Because of
+     this, types and terms share a common syntax.  All types are terms,
+     but not all terms are types:
+
+     .. insertprodn type type
+
+     .. prodn::
+        type ::= @term
+
+     Intuitively, types may be viewed as sets containing terms.  We
+     say that a type is :gdef:`inhabited` if it contains at least one
+     term (i.e. if we can find a term which is associated with this
+     type).  We call such terms :gdef:`witness`\es.  Note that deciding
+     whether a type is inhabited is `undecidable
+     <https://en.wikipedia.org/wiki/Undecidable_problem>`_.
+
+     Formally, types can be used to construct logical foundations for
+     mathematics alternative to the standard `"set theory"
+     <https://en.wikipedia.org/wiki/Set_theory>`_: we call such
+     logical foundations `"type theories"
+     <https://en.wikipedia.org/wiki/Type_theory>`_.  |Coq| is based on
+     the Calculus of Inductive Constructions, which is a particular
+     instance of type theory.
+
+   sentence
+
+     |Coq| documents are made of a series of sentences that contain
+     :term:`commands <command>` or :term:`tactics <tactic>`, generally
+     terminated with a period and optionally decorated with
+     :term:`attributes <attribute>`.
+
+     .. insertprodn document sentence
+
+     .. prodn::
+        document ::= {* @sentence }
+        sentence ::= {? @attributes } @command .
+        | {? @attributes } {? @num : } @query_command .
+        | {? @attributes } {? @toplevel_selector } @ltac_expr {| . | ... }
+        | @control_command
+
+     :n:`@ltac_expr` syntax supports both simple and compound
+     :term:`tactics <tactic>`.  For example: ``split`` is a simple
+     tactic while ``split; auto`` combines two simple tactics.
+
+   command
+
+     A :production:`command` can be used to modify the state of a |Coq|
+     document, for instance by declaring a new object, or to get
+     information about the current state.
+
+     By convention, command names begin with uppercase letters.
+     Commands appear in the HTML documentation in blue or gray boxes
+     after the label "Command".  In the pdf, they appear after the
+     boldface label "Command:".  Commands are listed in the
+     :ref:`command_index`.  Example:
+
+     .. cmd:: Comments {* @string }
+
+        This command prints "Comments ok" and does not change anything
+        to the state of the document.
+
+   tactic
+
+     Tactics specify how to transform the current proof state as a
+     step in creating a proof.  They are syntactically valid only when
+     |Coq| is in proof mode, such as after a :cmd:`Theorem` command
+     and before any subsequent proof-terminating command such as
+     :cmd:`Qed`.  See :ref:`proofhandling` for more on proof mode.
+
+     By convention, tactic names begin with lowercase letters.  Tactic
+     appear in the HTML documentation in blue or gray boxes after the
+     label "Tactic".  In the pdf, they appear after the boldface label
+     "Tactic:".  Tactics are listed in the :ref:`tactic_index`.
+
+Settings
+--------
+
+There are several mechanisms for changing the behavior of |Coq|.  The
+:term:`attribute` mechanism is used to modify the behavior of a single
+:term:`sentence`.  The :term:`flag`, :term:`option` and :term:`table`
+mechanisms are used to modify the behavior of |Coq| more globally in a
+document or project.
+
+.. _attributes:
 
 Attributes
------------
+~~~~~~~~~~
+
+An :gdef:`attribute` modifies the behavior of a single sentence.
+Syntactically, most commands and tactics can be decorated with
+attributes (cf. :n:`@sentence`), but attributes not supported by the
+command or tactic will trigger :warn:`This command does not support
+this attribute`.
 
-.. insertprodn all_attrs legacy_attr
+.. insertprodn attributes legacy_attr
 
 .. prodn::
-   all_attrs ::= {* #[ {*, @attr } ] } {* @legacy_attr }
-   attr ::= @ident {? @attr_value }
+   attributes ::= {* #[ {*, @attribute } ] } {* @legacy_attr }
+   attribute ::= @ident {? @attr_value }
    attr_value ::= = @string
-   | ( {*, @attr } )
+   | ( {*, @attribute } )
    legacy_attr ::= {| Local | Global }
    | {| Polymorphic | Monomorphic }
    | {| Cumulative | NonCumulative }
    | Private
    | Program
 
-Attributes modify the behavior of a command or tactic.
-Syntactically, most commands and tactics can be decorated with attributes, but
-attributes not supported by the command or tactic will be flagged as errors.
-
 The order of top-level attributes doesn't affect their meaning.  ``#[foo,bar]``, ``#[bar,foo]``,
 ``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent.
 
@@ -128,22 +365,38 @@ Legacy attribute  New attribute
 `Program`         :attr:`program`
 ================  ================================
 
-.. warn:: Unsupported attribute
+Attributes appear in the HTML documentation in blue or gray boxes
+after the label "Attribute".  In the pdf, they appear after the
+boldface label "Attribute:".  Attributes are listed in the
+:ref:`attribute_index`.
+
+.. warn:: This command does not support this attribute: @ident.
+   :name: This command does not support this attribute
+
+   This warning is configured to behave as an error by default.  You
+   may turn it into a normal warning by using the :opt:`Warnings` option:
+
+   .. coqtop:: none
 
-   This warning is an error by default. It is caused by using a
-   command with some attribute it does not understand.
+      Set Silent.
+
+   .. coqtop:: all warn
+
+      Set Warnings "unsupported-attributes".
+      #[ foo ] Comments.
 
 .. _flags-options-tables:
 
 Flags, Options and Tables
------------------------------
+~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Coq has many settings to control its behavior.  Setting types include flags, options
-and tables:
+The following types of settings can be used to change the behavior of |Coq| in
+subsequent commands and tactics (see :ref:`set_unset_scope_qualifiers` for a
+more precise description of the scope of these settings):
 
-* A *flag* has a boolean value, such as :flag:`Asymmetric Patterns`.
-* An *option* generally has a numeric or string value, such as :opt:`Firstorder Depth`.
-* A *table* contains a set of strings or qualids.
+* A :gdef:`flag` has a boolean value, such as :flag:`Universe Polymorphism`.
+* An :gdef:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`.
+* A :gdef:`table` contains a set of :token:`string`\s or :token:`qualid`\s.
 * In addition, some commands provide settings, such as :cmd:`Extraction Language`.
 
 .. FIXME Convert "Extraction Language" to an option.
@@ -151,6 +404,11 @@ and tables:
 Flags, options and tables are identified by a series of identifiers, each with an initial
 capital letter.
 
+Flags, options and tables appear in the HTML documentation in blue or
+gray boxes after the labels "Flag", "Option" and "Table".  In the pdf,
+they appear after a boldface label.  They are listed in the
+:ref:`options_index`.
+
 .. cmd:: Set @setting_name {? {| @int | @string } }
    :name: Set
 
@@ -172,10 +430,10 @@ capital letter.
       This warning message can be raised by :cmd:`Set` and
       :cmd:`Unset` when :n:`@setting_name` is unknown.  It is a
       warning rather than an error because this helps library authors
-      produce Coq code that is compatible with several Coq versions.
+      produce |Coq| code that is compatible with several |Coq| versions.
       To preserve the same behavior, they may need to set some
       compatibility flags or options that did not exist in previous
-      Coq versions.
+      |Coq| versions.
 
 .. cmd:: Unset @setting_name
    :name: Unset
@@ -198,7 +456,7 @@ capital letter.
 
    If :n:`@setting_name` is a flag or option, prints its current value.
    If :n:`@setting_name` is a table: if the `for` clause is specified, reports
-   whether the table contains each specified value, otherise this is equivalent to
+   whether the table contains each specified value, otherwise this is equivalent to
    :cmd:`Print Table`.  The `for` clause is not valid for flags and options.
 
    .. exn:: There is no flag, option or table with this name: "@setting_name".
@@ -230,33 +488,33 @@ capital letter.
 .. _set_unset_scope_qualifiers:
 
 Locality attributes supported by :cmd:`Set` and :cmd:`Unset`
-````````````````````````````````````````````````````````````
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`,
 :attr:`global` and :attr:`export` locality attributes:
 
 * no attribute: the original setting is *not* restored at the end of
   the current module or section.
-* :attr:`local` (an alternative syntax is to use the ``Local``
-  prefix): the setting is applied within the current module or
-  section.  The original value of the setting is restored at the end
-  of the current module or section.
-* :attr:`export` (an alternative syntax is to use the ``Export``
-  prefix): similar to :attr:`local`, the original value of the setting
-  is restored at the end of the current module or section.  In
-  addition, if the value is set in a module, then :cmd:`Import`\-ing
-  the module sets the option or flag.
-* :attr:`global` (an alternative syntax is to use the ``Global``
-  prefix): the original setting is *not* restored at the end of the
-  current module or section.  In addition, if the value is set in a
-  file, then :cmd:`Require`\-ing the file sets the option.
+* :attr:`local` (or alternatively, the ``Local`` prefix): the setting
+  is applied within the current module or section.  The original value
+  of the setting is restored at the end of the current module or
+  section.
+* :attr:`export` (or alternatively, the ``Export`` prefix): similar to
+  :attr:`local`, the original value of the setting is restored at the
+  end of the current module or section.  In addition, if the value is
+  set in a module, then :cmd:`Import`\-ing the module sets the option
+  or flag.
+* :attr:`global` (or alternatively, the ``Global`` prefix): the
+  original setting is *not* restored at the end of the current module
+  or section.  In addition, if the value is set in a file, then
+  :cmd:`Require`\-ing the file sets the option.
 
 Newly opened modules and sections inherit the current settings.
 
 .. note::
 
-   The use of the :attr:`global` attribute with the :cmd:`Set` and
-   :cmd:`Unset` commands is discouraged.  If your goal is to define
+   We discourage using the :attr:`global` attribute with the :cmd:`Set` and
+   :cmd:`Unset` commands.  If your goal is to define
    project-wide settings, you should rather use the command-line
    arguments ``-set`` and ``-unset`` for setting flags and options
    (cf. :ref:`command-line-options`).
diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst
index 5ee960d99b..5e83672463 100644
--- a/doc/sphinx/language/core/index.rst
+++ b/doc/sphinx/language/core/index.rst
@@ -6,23 +6,26 @@ Core language
 
 At the heart of the Coq proof assistant is the Coq kernel.  While
 users have access to a language with many convenient features such as
-notations, implicit arguments, etc. (that are presented in the
-:ref:`next chapter <extensions>`), such complex terms get translated
-down to a core language (the Calculus of Inductive Constructions) that
-the kernel understands, and which we present here.  Furthermore, while
-users can build proofs interactively using tactics (see Chapter
+:ref:`notations <syntax-extensions-and-notation-scopes>`,
+:ref:`implicit arguments <ImplicitArguments>`, etc.  (presented in the
+:ref:`next chapter <extensions>`), those features are translated into
+the core language (the Calculus of Inductive Constructions) that the
+kernel understands, which we present here.  Furthermore, while users
+can build proofs interactively using tactics (see Chapter
 :ref:`writing-proofs`), the role of these tactics is to incrementally
 build a "proof term" which the kernel will verify.  More precisely, a
-proof term is a term of the Calculus of Inductive Constructions whose
-type corresponds to a theorem statement.  The kernel is a type checker
-which verifies that terms have their expected type.
+proof term is a :term:`term` of the Calculus of Inductive
+Constructions whose :term:`type` corresponds to a theorem statement.
+The kernel is a type checker which verifies that terms have their
+expected types.
 
-This separation between the kernel on the one hand and the elaboration
-engine and tactics on the other hand follows what is known as the "de
-Bruijn criterion" (keeping a small and well delimited trusted code
+This separation between the kernel on one hand and the
+:ref:`elaboration engine <extensions>` and :ref:`tactics
+<writing-proofs>` on the other follows what is known as the :gdef:`de
+Bruijn criterion` (keeping a small and well delimited trusted code
 base within a proof assistant which can be much more complex).  This
-separation makes it possible to reduce the trust in the whole system
-to trusting a smaller, critical component: the kernel.  In particular,
+separation makes it necessary to trust only a smaller, critical
+component (the kernel) instead of the entire system.  In particular,
 users may rely on external plugins that provide advanced and complex
 tactics without fear of these tactics being buggy, because the kernel
 will have to check their output.
@@ -30,6 +33,7 @@ will have to check their output.
 .. toctree::
    :maxdepth: 1
 
+   basic
    ../gallina-specification-language
    ../cic
    records
diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index 928378f55e..0080f1d052 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -15,14 +15,17 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
 .. cmd:: {| Record | Structure } @record_definition {* with @record_definition }
    :name: Record; Structure
 
-   .. insertprodn record_definition field_body
+   .. insertprodn record_definition field_def
 
    .. prodn::
       record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations }
-      record_field ::= {* #[ {*, @attr } ] } @name {? @field_body } {? %| @num } {? @decl_notations }
+      record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @num } {? @decl_notations }
       field_body ::= {* @binder } @of_type
       | {* @binder } @of_type := @term
       | {* @binder } := @term
+      term_record ::= %{%| {* @field_def } %|%}
+      field_def ::= @qualid {* @binder } := @term
+
 
    Each :n:`@record_definition` defines a record named by :n:`@ident_decl`.
    The constructor name is given by :n:`@ident`.