diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 11 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 22 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 15 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 15 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 21 |
8 files changed, 68 insertions, 33 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index f7fd4b9146..e507a224c6 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -407,12 +407,11 @@ length, by writing .. coqtop:: in - Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : - listn (n + m) := - match l in listn n, l' return listn (n + m) with - | niln, x => x - | consn n' a y, x => consn (n' + m) a (concat n' y m x) - end. + Check (fun n (a b: listn n) => + match a, b with + | niln, b0 => tt + | consn n' a y, bS => tt + end). we have a copy of :g:`b` in type :g:`listn 0` resp. :g:`listn (S n')`. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index c0c4539564..23cbd76eda 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -325,6 +325,12 @@ Coercions and Modules This option makes it possible to recover the behavior of the versions of |Coq| prior to 8.3. +.. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it. + + This warning is emitted when typechecking relies on a coercion + contained in a module that has not been explicitely imported. It helps + migrating code and stop relying on the option above. + Examples -------- diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 1e92d01125..f7a431ef29 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -26,7 +26,9 @@ Description of ``omega`` .. tacv:: romega :name: romega - To be documented. + .. deprecated:: 8.9 + + Use :tacn:`lia` instead. Arithmetical goals recognized by ``omega`` ------------------------------------------ diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 3d3a1b11b1..35f45e2e0e 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1025,8 +1025,26 @@ the Type hierarchy. Template polymorphism +++++++++++++++++++++ -Inductive types declared in :math:`\Type` are polymorphic over their arguments -in :math:`\Type`. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` +Inductive types can be made polymorphic over their arguments +in :math:`\Type`. + +.. opt:: Auto Template Polymorphism + + This option, enabled by default, makes every inductive type declared + at level :math:`Type` (without annotations or hiding it behind a + definition) template polymorphic. + + This can be prevented using the ``notemplate`` attribute. + + An inductive type can be forced to be template polymorphic using the + ``template`` attribute. + + Template polymorphism and universe polymorphism (see Chapter + :ref:`polymorphicuniverses`) are incompatible, so if the later is + enabled it will prevail over automatic template polymorphism and + cause an error when using the ``template`` attribute. + +If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. Especially, if :math:`A` is well-typed in some global environment and local context, then :math:`A_{/s}` is typable by typability of all products in the diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 218a19c2e5..b9a4d2a7bd 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -268,13 +268,12 @@ file timing data: + ``print-pretty-timed-diff`` - this target builds a table of timing - changes between two compilations; run ``make make-pretty-timed-before`` to - build the log of the “before” times, and run ``make make-pretty-timed- - after`` to build the log of the “after” times. The table is printed on - the command line, and stored in ``time-of-build-both.log``. This target is - most useful for profiling the difference between two commits to a - repo. + this target builds a table of timing changes between two compilations; run + ``make make-pretty-timed-before`` to build the log of the “before” times, + and run ``make make-pretty-timed-after`` to build the log of the “after” + times. The table is printed on the command line, and stored in + ``time-of-build-both.log``. This target is most useful for profiling the + difference between two commits in a repository. .. note:: This target requires ``python`` to build the table. @@ -331,7 +330,9 @@ line timing data: Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] 0.239 secs (0.236u,0.s) + ``print-pretty-single-time-diff`` + :: + print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing this target will make a sorted table of the per-line timing differences diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 7608ea7245..70d46e034a 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -107,7 +107,7 @@ mode but it can also be used in toplevel definitions as shown below. : | solve [ `expr` | ... | `expr` ] : | idtac [ `message_token` ... `message_token`] : | fail [`natural`] [`message_token` ... `message_token`] - : | fresh | fresh `string` | fresh `qualid` + : | fresh [ `component` … `component` ] : | context `ident` [`term`] : | eval `redexpr` in `term` : | type of `term` @@ -125,6 +125,7 @@ mode but it can also be used in toplevel definitions as shown below. : | () : | `integer` : | ( `expr` ) + component : `string` | `qualid` message_token : `string` | `ident` | `integer` tacarg : `qualid` : | () @@ -946,12 +947,10 @@ expression returns an identifier: .. tacn:: fresh {* component} It evaluates to an identifier unbound in the goal. This fresh identifier - is obtained by concatenating the value of the :n:`@component`s (each of them + is obtained by concatenating the value of the :n:`@component`\ s (each of them is, either a :n:`@qualid` which has to refer to a (unqualified) name, or directly a name denoted by a :n:`@string`). - .. I don't understand this component thing. Couldn't we give the grammar? - If the resulting name is already used, it is padded with a number so that it becomes fresh. If no component is given, the name is a fresh derivative of the name ``H``. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 7c3ea1a28c..8656e5eb3e 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -444,11 +444,16 @@ not its name, one usually uses “arrow” abstractions for prenex arguments, or the ``(_ : term)`` syntax for inner arguments. In |SSR|, the latter can be replaced by the open syntax ``of term`` or (equivalently) ``& term``, which are both syntactically equivalent to a -``(_ : term)`` expression. +``(_ : term)`` expression. This feature almost behaves as the +following extension of the binder syntax: -For instance, the usual two-constructor polymorphic type list, i.e. -the one of the standard List library, can be defined by the following -declaration: +.. prodn:: + binder += & @term | of @term + +Caveat: ``& T`` and ``of T`` abbreviations have to appear at the end +of a binder list. For instance, the usual two-constructor polymorphic +type list, i.e. the one of the standard ``List`` library, can be +defined by the following declaration: .. example:: @@ -5387,7 +5392,7 @@ Tacticals discharge :ref:`discharge_ssr` -.. prodn:: tactic += @tacitc => {+ @i_item } +.. prodn:: tactic += @tactic => {+ @i_item } introduction see :ref:`introduction_ssr` diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index b46382dbbf..4c0e85bdd4 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -949,16 +949,25 @@ Interpretation scopes can include an interpretation for numerals and strings. However, this is only made possible at the Objective Caml level. -See :ref:`above <NotationSyntax>` for the syntax of notations including the -possibility to declare them in a given scope. Here is a typical example which -declares the notation for conjunction in the scope ``type_scope``. +.. cmd:: Declare Scope @scope + + This adds a new scope named :n:`@scope`. Note that the initial + state of Coq declares by default the following interpretation scopes: + ``core_scope``, ``type_scope``, ``function_scope``, ``nat_scope``, + ``bool_scope``, ``list_scope``, ``int_scope``, ``uint_scope``. + +The syntax to associate a notation to a scope is given +:ref:`above <NotationSyntax>`. Here is a typical example which declares the +notation for conjunction in the scope ``type_scope``. .. coqtop:: in Notation "A /\ B" := (and A B) : type_scope. .. note:: A notation not defined in a scope is called a *lonely* - notation. + notation. No example of lonely notations can be found in the + initial state of Coq though. + Global interpretation rules for notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -977,10 +986,6 @@ interpretation: otherwise said, only the order of lonely interpretations and opening of scopes matters, and not the declaration of interpretations within a scope). -The initial state of Coq declares three interpretation scopes and no -lonely notations. These scopes, in opening order, are ``core_scope``, -``type_scope`` and ``nat_scope``. - .. cmd:: Open Scope @scope The command to add a scope to the interpretation scope stack is |