diff options
Diffstat (limited to 'doc')
6 files changed, 28 insertions, 24 deletions
diff --git a/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst new file mode 100644 index 0000000000..1d30d16664 --- /dev/null +++ b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst @@ -0,0 +1,6 @@ +- **Added:** + Notations declared with the ``where`` clause in the declaration of + inductive types, coinductive types, record fields, fixpoints and + cofixpoints now support the ``only parsing`` modifier + (`#11602 <https://github.com/coq/coq/pull/11602>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/11429-zify-optimisation.rst b/doc/changelog/04-tactics/11429-zify-optimisation.rst new file mode 100644 index 0000000000..ce5bfa4aad --- /dev/null +++ b/doc/changelog/04-tactics/11429-zify-optimisation.rst @@ -0,0 +1,3 @@ +- **Changed** + Improve the efficiency of `zify` by rewritting the remaining Ltac code in OCaml. + (`#11429 <https://github.com/coq/coq/pull/11429>`_, by Frédéric Besson). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst b/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst new file mode 100644 index 0000000000..77fa556321 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst @@ -0,0 +1,9 @@ +- **Changed:** + Recursive OCaml loadpaths are not supported anymore; the command + ``Add Rec ML Path`` has been removed; :cmd:`Add ML Path` is now the + preferred one. We have also dropped support for the non-qualified + version of the :cmd:`Add LoadPath` command, that is to say, + the ``Add LoadPath dir`` version; now, + you must always specify a prefix now using ``Add Loadpath dir as Prefix.`` + (`#11618 <https://github.com/coq/coq/pull/11618>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 6c1d83b3b8..b9e181dd94 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -24,7 +24,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining record : `record_keyword` `record_body` with … with `record_body` record_keyword : Record | Inductive | CoInductive record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. - field : `ident` [ `binders` ] : `type` [ where `notation` ] + field : `ident` [ `binders` ] : `type` [ `decl_notations` ] : `ident` [ `binders` ] [: `type` ] := `term` .. cmd:: {| Record | Structure } @inductive_definition {* with @inductive_definition } @@ -35,8 +35,10 @@ expressions. In this sense, the :cmd:`Record` construction allows defining the default name :n:`Build_@ident`, where :token:`ident` is the record name, is used. If :token:`sort` is omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the names of fields. For a given field :token:`ident`, its type is :n:`forall {* @binder }, @type`. - Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the - order of the fields is important. Finally, :token:`binders` are parameters of the record. + Notice that the type of a particular identifier may depend on a previously-given identifier. Thus the + order of the fields is important. The record can depend as a whole on parameters :token:`binders` + and each field can also depend on its own :token:`binders`. Finally, notations can be attached to + fields using the :n:`decl_notations` annotation. :cmd:`Record` and :cmd:`Structure` are synonyms. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a38c26c2b3..d1f3dcc309 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -745,11 +745,6 @@ the toplevel, and using them in source files is discouraged. :n:`-Q @string @dirpath`. It adds the physical directory string to the current |Coq| loadpath and maps it to the logical directory dirpath. - .. cmdv:: Add LoadPath @string - - Performs as :n:`Add LoadPath @string @dirpath` but - for the empty directory path. - .. cmd:: Add Rec LoadPath @string as @dirpath @@ -757,11 +752,6 @@ the toplevel, and using them in source files is discouraged. :n:`-R @string @dirpath`. It adds the physical directory string and all its subdirectories to the current |Coq| loadpath. - .. cmdv:: Add Rec LoadPath @string - - Works as :n:`Add Rec LoadPath @string as @dirpath` but for the empty - logical directory path. - .. cmd:: Remove LoadPath @string @@ -784,12 +774,6 @@ the toplevel, and using them in source files is discouraged. loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`). -.. cmd:: Add Rec ML Path @string - - This command adds the directory :n:`@string` and all its subdirectories to - the current OCaml loadpath (see the command :cmd:`Declare ML Module`). - - .. cmd:: Print ML Path @string This command displays the current OCaml loadpath. This diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 9b4d7cf5fa..fd95a5cef4 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -909,10 +909,10 @@ notations are given below. The optional :production:`scope` is described in notation : [Local] Notation `string` := `term` [(`modifiers`)] [: `scope`]. : [Local] Infix `string` := `qualid` [(`modifiers`)] [: `scope`]. : [Local] Reserved Notation `string` [(`modifiers`)] . - : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. - : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. - : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. - : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. + : Inductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`]. + : CoInductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`]. + : Fixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`]. + : CoFixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`]. : [Local] Declare Custom Entry `ident`. modifiers : `modifier`, … , `modifier` modifier : at level `num` @@ -947,7 +947,7 @@ notations are given below. The optional :production:`scope` is described in .. prodn:: decl_notations ::= where @decl_notation {* and @decl_notation } - decl_notation ::= @string := @term1_extended {? : @ident } + decl_notation ::= @string := @term1_extended [(only parsing)] {? : @ident } .. note:: No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation. |