diff options
Diffstat (limited to 'doc')
23 files changed, 203 insertions, 113 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/02-specification-language/13106-doc-and-changelog-for-13106.rst b/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst new file mode 100644 index 0000000000..7fe69c39c1 --- /dev/null +++ b/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst @@ -0,0 +1,5 @@ +- **Removed:** + Undocumented and experimental forward class hint feature ``:>>``. + Use ``:>`` (see :n:`@of_type`) instead + (`#13106 <https://github.com/coq/coq/pull/13106>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst b/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst new file mode 100644 index 0000000000..006989e6b3 --- /dev/null +++ b/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Implicit arguments taken into account in defined fields of a record type declaration + (`#13166 <https://github.com/coq/coq/pull/13166>`_, + fixes `#13165 <https://github.com/coq/coq/issues/13165>`_, + by Hugo Herbelin). 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/04-tactics/12648-zify-int63.rst b/doc/changelog/04-tactics/12648-zify-int63.rst new file mode 100644 index 0000000000..ec7a1273e4 --- /dev/null +++ b/doc/changelog/04-tactics/12648-zify-int63.rst @@ -0,0 +1,3 @@ +- **Added:** + The :tacn:`zify` tactic provides support for primitive integers (module :g:`ZifyInt63`). + (`#12648 <https://github.com/coq/coq/pull/12648>`_, by Frédéric Besson). diff --git a/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst b/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst new file mode 100644 index 0000000000..0ab9a58e6f --- /dev/null +++ b/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst @@ -0,0 +1,6 @@ +- **Changed:** + Drop prefixes from grammar non-terminal names, + e.g. "constr:global" -> "global", "Prim.name" -> "name". + Visible in the output of :cmd:`Print Grammar` and :cmd:`Print Custom Grammar`. + (`#13096 <https://github.com/coq/coq/pull/13096>`_, + by Jim Fehrle). 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 Binary files differnew file mode 100644 index 0000000000..62bd9cccd0 --- /dev/null +++ b/doc/sphinx/_static/diffs-show-proof.png diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index ba5bac6489..b3a33ffeea 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -283,14 +283,19 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. .. tacn:: zify :name: zify - This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`. - By requiring the module ``ZifyBool``, the boolean type :g:`bool` and some comparison operators are also supported. + This tactic is internally called by :tacn:`lia` to support additional types, e.g., :g:`nat`, :g:`positive` and :g:`N`. + Additional support is provided by the following modules: + + + For boolean operators (e.g., :g:`Nat.leb`), require the module :g:`ZifyBool`. + + For comparison operators (e.g., :g:`Z.compare`), require the module :g:`ZifyComparison`. + + For native 63 bit integers, require the module :g:`ZifyInt63`. + :tacn:`zify` can also be extended by rebinding the tactics `Zify.zify_pre_hook` and `Zify.zify_post_hook` that are respectively run in the first and the last steps of :tacn:`zify`. + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``. + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``. - + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``. + + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot` and :g:`Z.rem`: either ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations`` or ``Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true)``. The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands. The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 479fa674f5..cda8a1b679 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -387,8 +387,8 @@ The syntax for adding a new ring is interpretation via ``Cp_phi`` (the evaluation function of power coefficient) is the original term, or returns ``InitialRing.NotConstant`` if not a constant coefficient (i.e. |L_tac| is the inverse function of - ``Cp_phi``). See files ``plugins/setoid_ring/ZArithRing.v`` - and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic + ``Cp_phi``). See files ``plugins/ring/ZArithRing.v`` + and ``plugins/ring/RealField.v`` for examples. By default the tactic does not recognize power expressions as ring expressions. :n:`sign @one_term` @@ -396,7 +396,7 @@ The syntax for adding a new ring is outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The term :token:`term` is a proof that a given sign function indicates expressions that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See - ``plugins/setoid_ring/InitialRing.v`` for examples of sign function. + ``plugins/ring/InitialRing.v`` for examples of sign function. :n:`div @one_term` allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with @@ -405,7 +405,7 @@ The syntax for adding a new ring is euclidean division function (:n:`@one_term` has to be a proof of ``Ring_theory.div_theory``). For example, this function is called when trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See - ``plugins/setoid_ring/InitialRing.v`` for examples of div function. + ``plugins/ring/InitialRing.v`` for examples of div function. :n:`closed [ {+ @qualid } ]` to be documented @@ -538,7 +538,7 @@ Dealing with fields The tactic must be loaded by ``Require Import Field``. New field structures can be declared to the system with the ``Add Field`` command (see below). The field of real numbers is defined in module ``RealField`` - (in ``plugins/setoid_ring``). It is exported by module ``Rbase``, so + (in ``plugins/ring``). It is exported by module ``Rbase``, so that requiring ``Rbase`` or ``Reals`` is enough to use the field tactics on real numbers. Rational numbers in canonical form are also declared as a field in the module ``Qcanon``. diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index fe10e345cd..41e1c30f0d 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -138,7 +138,7 @@ has type :n:`@type`. | {| Variable | Variables } assumpt ::= {+ @ident_decl } @of_type ident_decl ::= @ident {? @univ_decl } - of_type ::= {| : | :> | :>> } @type + of_type ::= {| : | :> } @type These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in the global context. The fact asserted by the :n:`@type` (or, equivalently, the existence 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/primitive.rst b/doc/sphinx/language/core/primitive.rst index 727177b23a..48647deeff 100644 --- a/doc/sphinx/language/core/primitive.rst +++ b/doc/sphinx/language/core/primitive.rst @@ -133,7 +133,7 @@ follows: Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a. Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j]. -The complete set of such operators can be obtained looking at the :g:`PArray` module. +The rest of these operators can be found in the :g:`PArray` module. These primitive declarations are regular axioms. As such, they must be trusted and are listed by the :g:`Print Assumptions` command. @@ -150,7 +150,16 @@ extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module can be taken from the kernel of Coq (see ``kernel/parray.ml``). -Primitive arrays expose a functional interface, but they are internally -implemented using a persistent data structure :cite:`ConchonFilliatre07wml`. -Update and access to an element in the most recent copy of an array are -constant time operations. +Coq's primitive arrays are persistent data structures. Semantically, a set operation +``t.[i <- a]`` represents a new array that has the same values as ``t``, except +at position ``i`` where its value is ``a``. The array ``t`` still exists, can +still be used and its values were not modified. Operationally, the implementation +of Coq's primitive arrays is optimized so that the new array ``t.[i <- a]`` does not +copy all of ``t``. The details are in section 2.3 of :cite:`ConchonFilliatre07wml`. +In short, the implementation keeps one version of ``t`` as an OCaml native array and +other versions as lists of modifications to ``t``. Accesses to the native array +version are constant time operations. However, accesses to versions where all the cells of +the array are modified have O(n) access time, the same as a list. The version that is kept as the native array +changes dynamically upon each get and set call: the current list of modifications +is applied to the native array and the lists of modifications of the other versions +are updated so that they still represent the same values. 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..edd93f2266 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 ------------------------------------------------ @@ -858,6 +878,11 @@ Controlling the effect of proof editing commands proved before starting the previous proof) and Coq will switch back to the proof of the previous assertion. +.. flag:: Printing Goal Names + + When turned on, the name of the goal is printed in interactive + proof mode, which can be useful in cases of cross references + between goals. Controlling memory usage ------------------------ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index e276a0edcb..4b1f312105 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4726,7 +4726,7 @@ Automating .. seealso:: - File plugins/setoid_ring/RealField.v for an example of instantiation, + File plugins/ring/RealField.v for an example of instantiation, theory theories/Reals for many examples of use of field. Non-logical tactics diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6ba53b581b..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 ~~~~~~~~~~~~~~~~~~ @@ -429,10 +446,6 @@ Displaying information about notations productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` and `tactic_then_gen` which are not shown and can't be printed. - The prefixes `tactic:`, `prim:`, `constr:` appearing in the output are meant to identify - what part of the grammar a nonterminal is from. If you examine nonterminal definitions - in the source code, they are identified only by the name following the colon. - Most of the grammar in the documentation was updated in 8.12 to make it accurate and readable. This was done using a new developer tool that extracts the grammar from the source code, edits it and inserts it into the documentation files. While the @@ -467,11 +480,11 @@ Displaying information about notations `tactic_expr`, designated as "5", "4" and "3". Level 3 is right-associative, which applies to the productions within it, such as the `try` construct:: - Entry tactic:tactic_expr is + Entry tactic_expr is [ "5" RIGHTA - [ tactic:binder_tactic ] + [ binder_tactic ] | "4" LEFTA - [ SELF; ";"; tactic:binder_tactic + [ SELF; ";"; binder_tactic | SELF; ";"; SELF | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ] | "3" RIGHTA diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index f39c50238a..4d2972ef8f 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -50,6 +50,7 @@ theories/micromega/ZCoeff.v theories/micromega/ZMicromega.v theories/micromega/ZifyInst.v theories/micromega/ZifyBool.v +theories/micromega/ZifyInt63.v theories/micromega/ZifyComparison.v theories/micromega/ZifyClasses.v theories/micromega/ZifyPow.v diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index a22f7ae9f3..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 *) ] @@ -615,7 +615,7 @@ of_type_with_opt_coercion: [ ] of_type_with_opt_coercion: [ -| [ ":" | ":>" | ":>>" ] type +| [ ":" | ":>" ] type ] attribute_value: [ diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 0ac652c0db..177abe53fc 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -909,14 +909,17 @@ let apply_splice g edit_map = List.iter (fun b -> let (nt0, prods0) = b in let rec splice_loop nt prods cnt = - let max_cnt = 10 in - let (nt', prods') = edit_rule g edit_map nt prods in - if cnt > max_cnt then - error "Splice for '%s' not done after %d iterations\n" nt0 max_cnt; - if nt' = nt && prods' = prods then - (nt', prods') - else - splice_loop nt' prods' (cnt+1) + if cnt >= 10 then begin + error "Splice for '%s' not done after %d iterations. Current value is:\n" nt0 cnt; + List.iter (fun prod -> Printf.eprintf " %s\n" (prod_to_str prod)) prods; + (nt, prods) + end else begin + let (nt', prods') = edit_rule g edit_map nt prods in + if nt' = nt && prods' = prods then + (nt, prods) + else + splice_loop nt' prods' (cnt+1) + end in let (nt', prods') = splice_loop nt0 prods0 0 in g_update_prods g nt' prods') diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index ba07e6df0d..2a7b283f55 100644 --- a/doc/tools/docgram/dune +++ b/doc/tools/docgram/dune @@ -24,7 +24,7 @@ (glob_files %{project_root}/plugins/nsatz/*.mlg) (glob_files %{project_root}/plugins/omega/*.mlg) (glob_files %{project_root}/plugins/rtauto/*.mlg) - (glob_files %{project_root}/plugins/setoid_ring/*.mlg) + (glob_files %{project_root}/plugins/ring/*.mlg) (glob_files %{project_root}/plugins/syntax/*.mlg) (glob_files %{project_root}/user-contrib/Ltac2/*.mlg) ; Sphinx files diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 2ee8e4347e..73641976e3 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -685,10 +685,10 @@ command: [ | "Show" "Zify" "UnOpSpec" (* micromega plugin *) | "Show" "Zify" "BinOpSpec" (* micromega plugin *) | "Show" "Zify" "Spec" (* micromega plugin *) -| "Add" "Ring" ident ":" constr OPT ring_mods (* setoid_ring plugin *) -| "Print" "Rings" (* setoid_ring plugin *) -| "Add" "Field" ident ":" constr OPT field_mods (* setoid_ring plugin *) -| "Print" "Fields" (* setoid_ring plugin *) +| "Add" "Ring" ident ":" constr OPT ring_mods (* ring plugin *) +| "Print" "Rings" (* ring plugin *) +| "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) +| "Print" "Fields" (* ring plugin *) | "Number" "Notation" reference reference reference ":" ident numnotoption | "Numeral" "Notation" reference reference reference ":" ident numnotoption | "String" "Notation" reference reference reference ":" ident @@ -986,10 +986,7 @@ constructor: [ ] of_type_with_opt_coercion: [ -| ":>>" -| ":>" ">" | ":>" -| ":" ">" ">" | ":" ">" | ":" ] @@ -1743,11 +1740,11 @@ simple_tactic: [ | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" constr (* nsatz plugin *) | "omega" (* omega plugin *) +| "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" -| "protect_fv" string "in" ident (* setoid_ring plugin *) -| "protect_fv" string (* setoid_ring plugin *) -| "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* setoid_ring plugin *) -| "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr (* setoid_ring plugin *) ] mlname: [ @@ -1761,7 +1758,6 @@ int_or_id: [ ] language: [ -| "Ocaml" (* extraction plugin *) | "OCaml" (* extraction plugin *) | "Haskell" (* extraction plugin *) | "Scheme" (* extraction plugin *) @@ -2532,31 +2528,31 @@ induction_clause_list: [ ] ring_mod: [ -| "decidable" constr (* setoid_ring plugin *) -| "abstract" (* setoid_ring plugin *) -| "morphism" constr (* setoid_ring plugin *) -| "constants" "[" tactic "]" (* setoid_ring plugin *) -| "closed" "[" LIST1 global "]" (* setoid_ring plugin *) -| "preprocess" "[" tactic "]" (* setoid_ring plugin *) -| "postprocess" "[" tactic "]" (* setoid_ring plugin *) -| "setoid" constr constr (* setoid_ring plugin *) -| "sign" constr (* setoid_ring plugin *) -| "power" constr "[" LIST1 global "]" (* setoid_ring plugin *) -| "power_tac" constr "[" tactic "]" (* setoid_ring plugin *) -| "div" constr (* setoid_ring plugin *) +| "decidable" constr (* ring plugin *) +| "abstract" (* ring plugin *) +| "morphism" constr (* ring plugin *) +| "constants" "[" tactic "]" (* ring plugin *) +| "closed" "[" LIST1 global "]" (* ring plugin *) +| "preprocess" "[" tactic "]" (* ring plugin *) +| "postprocess" "[" tactic "]" (* ring plugin *) +| "setoid" constr constr (* ring plugin *) +| "sign" constr (* ring plugin *) +| "power" constr "[" LIST1 global "]" (* ring plugin *) +| "power_tac" constr "[" tactic "]" (* ring plugin *) +| "div" constr (* ring plugin *) ] ring_mods: [ -| "(" LIST1 ring_mod SEP "," ")" (* setoid_ring plugin *) +| "(" LIST1 ring_mod SEP "," ")" (* ring plugin *) ] field_mod: [ -| ring_mod (* setoid_ring plugin *) -| "completeness" constr (* setoid_ring plugin *) +| ring_mod (* ring plugin *) +| "completeness" constr (* ring plugin *) ] field_mods: [ -| "(" LIST1 field_mod SEP "," ")" (* setoid_ring plugin *) +| "(" LIST1 field_mod SEP "," ")" (* ring plugin *) ] numnotoption: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index aae96fc966..61befe9f1f 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -114,7 +114,7 @@ ident_decl: [ ] of_type: [ -| [ ":" | ":>" | ":>>" ] type +| [ ":" | ":>" ] type ] qualid: [ @@ -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: [ @@ -892,10 +892,10 @@ command: [ | "Show" "Zify" "UnOpSpec" (* micromega plugin *) | "Show" "Zify" "BinOpSpec" (* micromega plugin *) | "Show" "Zify" "Spec" (* micromega plugin *) -| "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" ) (* setoid_ring plugin *) -| "Print" "Rings" (* setoid_ring plugin *) -| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* setoid_ring plugin *) -| "Print" "Fields" (* setoid_ring plugin *) +| "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" ) (* ring plugin *) +| "Print" "Rings" (* ring plugin *) +| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) +| "Print" "Fields" (* ring plugin *) | "Number" "Notation" qualid qualid qualid ":" ident OPT numeral_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST0 qualid @@ -1268,7 +1268,6 @@ int_or_id: [ ] language: [ -| "Ocaml" (* extraction plugin *) | "OCaml" (* extraction plugin *) | "Haskell" (* extraction plugin *) | "Scheme" (* extraction plugin *) @@ -1280,23 +1279,23 @@ fun_scheme_arg: [ ] ring_mod: [ -| "decidable" one_term (* setoid_ring plugin *) -| "abstract" (* setoid_ring plugin *) -| "morphism" one_term (* setoid_ring plugin *) -| "constants" "[" ltac_expr "]" (* setoid_ring plugin *) -| "preprocess" "[" ltac_expr "]" (* setoid_ring plugin *) -| "postprocess" "[" ltac_expr "]" (* setoid_ring plugin *) -| "setoid" one_term one_term (* setoid_ring plugin *) -| "sign" one_term (* setoid_ring plugin *) -| "power" one_term "[" LIST1 qualid "]" (* setoid_ring plugin *) -| "power_tac" one_term "[" ltac_expr "]" (* setoid_ring plugin *) -| "div" one_term (* setoid_ring plugin *) -| "closed" "[" LIST1 qualid "]" (* setoid_ring plugin *) +| "decidable" one_term (* ring plugin *) +| "abstract" (* ring plugin *) +| "morphism" one_term (* ring plugin *) +| "constants" "[" ltac_expr "]" (* ring plugin *) +| "preprocess" "[" ltac_expr "]" (* ring plugin *) +| "postprocess" "[" ltac_expr "]" (* ring plugin *) +| "setoid" one_term one_term (* ring plugin *) +| "sign" one_term (* ring plugin *) +| "power" one_term "[" LIST1 qualid "]" (* ring plugin *) +| "power_tac" one_term "[" ltac_expr "]" (* ring plugin *) +| "div" one_term (* ring plugin *) +| "closed" "[" LIST1 qualid "]" (* ring plugin *) ] field_mod: [ -| ring_mod (* setoid_ring plugin *) -| "completeness" one_term (* setoid_ring plugin *) +| ring_mod (* ring plugin *) +| "completeness" one_term (* ring plugin *) ] numeral_modifier: [ @@ -1642,8 +1641,8 @@ simple_tactic: [ | "nsatz_compute" one_term (* nsatz plugin *) | "omega" (* omega plugin *) | "protect_fv" string OPT ( "in" ident ) -| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* setoid_ring plugin *) -| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* setoid_ring plugin *) +| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) +| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) | match_key OPT "reverse" "goal" "with" OPT "|" LIST1 ( goal_pattern "=>" ltac_expr ) SEP "|" "end" | match_key ltac_expr "with" OPT "|" LIST1 ( match_pattern "=>" ltac_expr ) SEP "|" "end" | "classical_left" |
