diff options
Diffstat (limited to 'doc/sphinx')
| -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 | 26 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 15 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/detailed-tactic-examples.rst | 212 | ||||
| -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/proof-engine/tactics.rst | 24 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 169 |
10 files changed, 221 insertions, 268 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..ac0f0f8ea6 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -605,7 +605,7 @@ Subtyping rules At the moment, we did not take into account one rule between universes which says that any term in a universe of index i is also a term in -the universe of index i+1 (this is the *cumulativity* rule of|Cic|). +the universe of index i+1 (this is the *cumulativity* rule of |Cic|). This property extends the equivalence relation of convertibility into a *subtyping* relation inductively defined by: @@ -640,7 +640,7 @@ a *subtyping* relation inductively defined by: respectively then .. math:: - E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t~w_1' … w_m' + E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t'~w_1' … w_m' (notice that :math:`t` and :math:`t'` are both fully applied, i.e., they have a sort as a type) if @@ -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/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 72dd79d930..bd16b70d02 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -417,218 +417,8 @@ the optional tactic of the ``Hint Rewrite`` command. Qed. -.. _quote: - -quote ------ - -The tactic ``quote`` allows using Barendregt’s so-called 2-level approach -without writing any ML code. Suppose you have a language ``L`` of -'abstract terms' and a type ``A`` of 'concrete terms' and a function ``f : L -> A``. -If ``L`` is a simple inductive datatype and ``f`` a simple fixpoint, -``quote f`` will replace the head of current goal by a convertible term of -the form ``(f t)``. ``L`` must have a constructor of type: ``A -> L``. - -Here is an example: - -.. coqtop:: in reset - - Require Import Quote. - -.. coqtop:: all - - Parameters A B C : Prop. - -.. coqtop:: all - - Inductive formula : Type := - | f_and : formula -> formula -> formula (* binary constructor *) - | f_or : formula -> formula -> formula - | f_not : formula -> formula (* unary constructor *) - | f_true : formula (* 0-ary constructor *) - | f_const : Prop -> formula (* constructor for constants *). - -.. coqtop:: all - - Fixpoint interp_f (f:formula) : Prop := - match f with - | f_and f1 f2 => interp_f f1 /\ interp_f f2 - | f_or f1 f2 => interp_f f1 \/ interp_f f2 - | f_not f1 => ~ interp_f f1 - | f_true => True - | f_const c => c - end. - -.. coqtop:: all - - Goal A /\ (A \/ True) /\ ~ B /\ (A <-> A). - -.. coqtop:: all - - quote interp_f. - -The algorithm to perform this inversion is: try to match the term with -right-hand sides expression of ``f``. If there is a match, apply the -corresponding left-hand side and call yourself recursively on sub- -terms. If there is no match, we are at a leaf: return the -corresponding constructor (here ``f_const``) applied to the term. - -When ``quote`` is not able to perform inversion properly, it will error out with -:exn:`quote: not a simple fixpoint`. - - -Introducing variables map -~~~~~~~~~~~~~~~~~~~~~~~~~ - -The normal use of quote is to make proofs by reflection: one defines a -function ``simplify : formula -> formula`` and proves a theorem -``simplify_ok: (f:formula)(interp_f (simplify f)) -> (interp_f f)``. Then, -one can simplify formulas by doing: - -.. coqtop:: in - - quote interp_f. - apply simplify_ok. - compute. - -But there is a problem with leafs: in the example above one cannot -write a function that implements, for example, the logical -simplifications :math:`A \wedge A \rightarrow A` or :math:`A \wedge -\lnot A \rightarrow \mathrm{False}`. This is because ``Prop`` is -impredicative. - -It is better to use that type of formulas: - -.. coqtop:: in reset - - Require Import Quote. - -.. coqtop:: in - - Parameters A B C : Prop. - -.. coqtop:: all - - Inductive formula : Set := - | f_and : formula -> formula -> formula - | f_or : formula -> formula -> formula - | f_not : formula -> formula - | f_true : formula - | f_atom : index -> formula. - -``index`` is defined in module ``Quote``. Equality on that type is -decidable so we are able to simplify :math:`A \wedge A` into :math:`A` -at the abstract level. - -When there are variables, there are bindings, and ``quote`` also -provides a type ``(varmap A)`` of bindings from index to any set -``A``, and a function ``varmap_find`` to search in such maps. The -interpretation function also has another argument, a variables map: - -.. coqtop:: all - - Fixpoint interp_f (vm:varmap Prop) (f:formula) {struct f} : Prop := - match f with - | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 - | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 - | f_not f1 => ~ interp_f vm f1 - | f_true => True - | f_atom i => varmap_find True i vm - end. - -``quote`` handles this second case properly: - -.. coqtop:: all - - Goal A /\ (B \/ A) /\ (A \/ ~ B). - -.. coqtop:: all - - quote interp_f. - -It builds ``vm`` and ``t`` such that ``(f vm t)`` is convertible with the -conclusion of current goal. - - -Combining variables and constants -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -One can have both variables and constants in abstracts terms; for -example, this is the case for the :tacn:`ring` tactic. Then one must provide to -``quote`` a list of *constructors of constants*. For example, if the list -is ``[O S]`` then closed natural numbers will be considered as constants -and other terms as variables. - -.. coqtop:: in reset - - Require Import Quote. - -.. coqtop:: in - - Parameters A B C : Prop. - -.. coqtop:: in - - Inductive formula : Type := - | f_and : formula -> formula -> formula - | f_or : formula -> formula -> formula - | f_not : formula -> formula - | f_true : formula - | f_const : Prop -> formula (* constructor for constants *) - | f_atom : index -> formula. - -.. coqtop:: in - - Fixpoint interp_f (vm:varmap Prop) (f:formula) {struct f} : Prop := - match f with - | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 - | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 - | f_not f1 => ~ interp_f vm f1 - | f_true => True - | f_const c => c - | f_atom i => varmap_find True i vm - end. - -.. coqtop:: in - - Goal A /\ (A \/ True) /\ ~ B /\ (C <-> C). - -.. coqtop:: all - - quote interp_f [ A B ]. - - -.. coqtop:: all - - Undo. - -.. coqtop:: all - - quote interp_f [ B C iff ]. - -.. warning:: - Since functional inversion is undecidable in the general case, - don’t expect miracles from it! - -.. tacv:: quote @ident in @term using @tactic - - ``tactic`` must be a functional tactic (starting with ``fun x =>``) and - will be called with the quoted version of term according to ``ident``. - -.. tacv:: quote @ident [{+ @ident}] in @term using @tactic - - Same as above, but will use the additional ``ident`` list to chose - which subterms are constants (see above). - -.. seealso:: - Comments from the source file ``plugins/quote/quote.ml`` - -.. seealso:: - The :tacn:`ring` tactic. - - Using the tactic language ---------------------------- +------------------------- About the cardinality of the set of natural numbers 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/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 241cdf5eea..fb121c82ec 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1345,8 +1345,8 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. changes in the goal, its use is strongly discouraged. .. tacv:: instantiate ( @num := @term ) in @ident -.. tacv:: instantiate ( @num := @term ) in ( Value of @ident ) -.. tacv:: instantiate ( @num := @term ) in ( Type of @ident ) +.. tacv:: instantiate ( @num := @term ) in ( value of @ident ) +.. tacv:: instantiate ( @num := @term ) in ( type of @ident ) These allow to refer respectively to existential variables occurring in a hypothesis or in the body or the type of a local definition. @@ -4217,26 +4217,6 @@ available after a ``Require Import FunInd``. functional inversion, this variant allows choosing which :n:`@qualid` is inverted. -.. tacn:: quote @ident - :name: quote - -This kind of inversion has nothing to do with the tactic :tacn:`inversion` -above. This tactic does :g:`change (@ident t)`, where `t` is a term built in -order to ensure the convertibility. In other words, it does inversion of the -function :n:`@ident`. This function must be a fixpoint on a simple recursive -datatype: see :ref:`quote` for the full details. - - -.. exn:: quote: not a simple fixpoint. - - Happens when quote is not able to perform inversion properly. - - -.. tacv:: quote @ident {* @ident} - - All terms that are built only with :n:`{* @ident}` will be considered by quote - as constants rather than variables. - Classical tactics ----------------- diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 5089a1b3e3..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 @@ -1372,6 +1377,154 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. + +Numeral notations +----------------- + +.. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. + + This command allows the user to customize the way numeral literals + are parsed and printed. + + The token :n:`@ident__1` should be the name of an inductive type, + while :n:`@ident__2` and :n:`@ident__3` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@ident__2` should have one of the following types: + + * :n:`Decimal.int -> @ident__1` + * :n:`Decimal.int -> option @ident__1` + * :n:`Decimal.uint -> @ident__1` + * :n:`Decimal.uint -> option @ident__1` + * :n:`Z -> @ident__1` + * :n:`Z -> option @ident__1` + + And the printing function :n:`@ident__3` should have one of the + following types: + + * :n:`@ident__1 -> Decimal.int` + * :n:`@ident__1 -> option Decimal.int` + * :n:`@ident__1 -> Decimal.uint` + * :n:`@ident__1 -> option Decimal.uint` + * :n:`@ident__1 -> Z` + * :n:`@ident__1 -> option Z` + + When parsing, the application of the parsing function + :n:`@ident__2` to the number will be fully reduced, and universes + of the resulting term will be refreshed. + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). + + When a literal larger than :token:`num` is parsed, a warning + message about possible stack overflow, resulting from evaluating + :n:`@ident__2`, will be displayed. + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). + + When a literal :g:`m` larger than :token:`num` is parsed, the + result will be :n:`(@ident__2 m)`, without reduction of this + application to a normal form. Here :g:`m` will be a + :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the + type of the parsing function :n:`@ident__2`. This allows for a + more compact representation of literals in types such as :g:`nat`, + and limits parse failures due to stack overflow. Note that a + warning will be emitted when an integer larger than :token:`num` + is parsed. Note that :n:`(abstract after @num)` has no effect + when :n:`@ident__2` lands in an :g:`option` type. + + .. exn:: Cannot interpret this number as a value of type @type + + The numeral notation registered for :token:`type` does not support + the given numeral. This error is given when the interpretation + function returns :g:`None`, or if the interpretation is registered + for only non-negative integers, and the given numeral is negative. + + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The parsing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The printing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @type is not an inductive type. + + Numeral notations can only be declared for inductive types with no + arguments. + + .. exn:: Unexpected term @term while parsing a numeral notation. + + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. + + .. exn:: Unexpected non-option term @term while parsing a numeral notation. + + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete numeral expressed as a decimal. They may not return + opaque constants. + + .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. + + The inductive type used to register the numeral notation is no + longer available in the environment. Most likely, this is because + the numeral notation was declared inside a functor for an + inductive type inside the functor. This use case is not currently + supported. + + Alternatively, you might be trying to use a primitive token + notation from a plugin which forgot to specify which module you + must :g:`Require` for access to that notation. + + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + + The type passed to :cmd:`Numeral Notation` must be a single + identifier. + + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + + Both functions passed to :cmd:`Numeral Notation` must be single + identifiers. + + .. exn:: The reference @ident was not found in the current environment. + + Identifiers passed to :cmd:`Numeral Notation` must exist in the + global environment. + + .. exn:: @ident is bound to a notation that does not denote a reference. + + Identifiers passed to :cmd:`Numeral Notation` must be global + references, or notations which denote to single identifiers. + + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(warning after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + + .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(abstract after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + Typically, this indicates that the fully computed representation + of numerals can be so large that non-tail-recursive OCaml + functions run out of stack space when trying to walk them. + + For example + + .. coqtop:: all + + Check 90000. + + .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. + + As noted above, the :n:`(abstract after @num)` directive has no + effect when :n:`@ident__2` lands in an :g:`option` type. + .. _TacticNotation: Tactic Notations |