diff options
Diffstat (limited to 'doc')
15 files changed, 60 insertions, 39 deletions
diff --git a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md new file mode 100644 index 0000000000..e0573a2c74 --- /dev/null +++ b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md @@ -0,0 +1,4 @@ +- Internal definitions generated by abstract-like tactics are now inlined + inside universe Qed-terminated polymorphic definitions, similarly to what + happens for their monomorphic counterparts, + (`#10439 <https://github.com/coq/coq/pull/10439>`_, by Pierre-Marie Pédrot). diff --git a/doc/changelog/02-specification-language/10049-bidi-app.rst b/doc/changelog/02-specification-language/10049-bidi-app.rst index 79678c5242..279bb9272a 100644 --- a/doc/changelog/02-specification-language/10049-bidi-app.rst +++ b/doc/changelog/02-specification-language/10049-bidi-app.rst @@ -1,6 +1,6 @@ - New annotation in `Arguments` for bidirectionality hints: it is now possible to tell type inference to use type information from the context once the `n` first arguments of an application are known. The syntax is: - `Arguments foo x y & z`. - `#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with - help from Enrico Tassi + `Arguments foo x y & z`. See :cmd:`Arguments (bidirectionality hints)` + (`#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with + help from Enrico Tassi). diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst index e3c3923348..2d17e569d3 100644 --- a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst +++ b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst @@ -7,6 +7,6 @@ + notation :g:`(p | q)` now potentially clashes with core pattern syntax, and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`. - see :ref:`extendedpatternmatching` for details + See :ref:`extendedpatternmatching` for details (`#10167 <https://github.com/coq/coq/pull/10167>`_, by Georges Gonthier). diff --git a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst index 21ec7f8e5b..71b10aaaf4 100644 --- a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst +++ b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst @@ -1,11 +1,11 @@ -- Function always opens a proof when used with a ``measure`` or ``wf`` +- :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf`` annotation, see :ref:`advanced-recursive-functions` for the updated documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, by Enrico Tassi). -- The legacy command Add Morphism always opens a proof and cannot be used +- The legacy command :cmd:`Add Morphism` always opens a proof and cannot be used inside a module type. In order to declare a module type parameter that - happens to be a morphism, use ``Parameter Morphism``. See + happens to be a morphism, use :cmd:`Declare Morphism`. See :ref:`deprecated_syntax_for_generalized_rewriting` for the updated documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, by Enrico Tassi). diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst index 01f2e893ed..bce5db5865 100644 --- a/doc/changelog/03-notations/10180-deprecate-notations.rst +++ b/doc/changelog/03-notations/10180-deprecate-notations.rst @@ -2,5 +2,5 @@ attribute. The former `compat` annotation for notations is deprecated, and its semantics changed. It is now made equivalent to using a `deprecated` attribute, and is no longer connected with the `-compat` - command-line flag. + command-line flag (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès). diff --git a/doc/changelog/04-tactics/09288-injection-as.rst b/doc/changelog/04-tactics/09288-injection-as.rst index 6a74551f06..0cb669778c 100644 --- a/doc/changelog/04-tactics/09288-injection-as.rst +++ b/doc/changelog/04-tactics/09288-injection-as.rst @@ -1,4 +1,4 @@ - Documented syntax :n:`injection @term as [= {+ @intropattern} ]` as an alternative to :n:`injection @term as {+ @simple_intropattern}` using - the standard :n:`@injection_intropattern` syntax (`#09288 - <https://github.com/coq/coq/pull/09288>`_, by Hugo Herbelin). + the standard :n:`@injection_intropattern` syntax (`#9288 + <https://github.com/coq/coq/pull/9288>`_, by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/10318-select-only-error.rst b/doc/changelog/04-tactics/10318-select-only-error.rst index 03ed15d948..b4f991316e 100644 --- a/doc/changelog/04-tactics/10318-select-only-error.rst +++ b/doc/changelog/04-tactics/10318-select-only-error.rst @@ -1,4 +1,4 @@ - The goal selector tactical ``only`` now checks that the goal range it is given is valid instead of ignoring goals out of the focus - range. (`#10318 <https://github.com/coq/coq/pull/10318>`_, by Gaëtan + range (`#10318 <https://github.com/coq/coq/pull/10318>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst index 78874cadb1..1c91800c65 100644 --- a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst +++ b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst @@ -1,5 +1,5 @@ - Deprecated flag `Refine Instance Mode` has been removed. - (`#09530 <https://github.com/coq/coq/pull/09530>`_, fixes + (`#9530 <https://github.com/coq/coq/pull/9530>`_, fixes `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890 <https://github.com/coq/coq/issues/3890>`_ and `#4638 <https://github.com/coq/coq/issues/4638>`_ diff --git a/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst b/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst new file mode 100644 index 0000000000..151c400b2c --- /dev/null +++ b/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst @@ -0,0 +1,5 @@ +- Improve the ambiguous paths warning to indicate which path is ambiguous with + new one + (`#10336 <https://github.com/coq/coq/pull/10336>`_, + closes `#3219 <https://github.com/coq/coq/issues/3219>`_, + by Kazuhiko Sakaguchi). diff --git a/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst b/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst new file mode 100644 index 0000000000..8bfd01d7a0 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst @@ -0,0 +1,5 @@ +- Coq now officially supports OCaml 4.08. + + see INSTALL files for details + (`#10471 <https://github.com/coq/coq/pull/10471>`_, + by Emilio Jesús Gallego Arias). diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 68ae5628db..9dd4700db5 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -9,4 +9,4 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decl_kinds.Definition ~opaque:false sigma udecl body None [] + ~kind:Decls.Definition ~opaque:false sigma udecl body None [] diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml index ba989b1bac..88afec14d5 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -2,14 +2,15 @@ type constr is given in the coq-dpdgraph plugin. *) let simple_body_access gref = + let open Names.GlobRef in match gref with - | Globnames.VarRef _ -> + | VarRef _ -> failwith "variables are not covered in this example" - | Globnames.IndRef _ -> + | IndRef _ -> failwith "inductive types are not covered in this example" - | Globnames.ConstructRef _ -> + | ConstructRef _ -> failwith "constructors are not covered in this example" - | Globnames.ConstRef cst -> + | ConstRef cst -> let cb = Environ.lookup_constant cst (Global.env()) in match Global.body_of_constant_body Library.indirect_accessor cb with | Some(e, _, _) -> EConstr.of_constr e diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index d5523e8561..7fee62179b 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -145,19 +145,25 @@ Declaring Coercions .. exn:: Cannot recognize @class as a source class of @qualid. :undocumented: - .. exn:: @qualid does not respect the uniform inheritance condition. + .. warn:: @qualid does not respect the uniform inheritance condition. :undocumented: .. exn:: Found target class ... instead of ... :undocumented: - .. warn:: Ambiguous path. + .. warn:: New coercion path ... is ambiguous with existing ... - When the coercion :token:`qualid` is added to the inheritance graph, - invalid coercion paths are ignored. The :cmd:`Coercion` command tries to check - that they are convertible with existing ones on the same classes. - The paths for which this check fails are displayed by a warning in the form - :g:`[f₁;..;fₙ] : C >-> D`. + When the coercion :token:`qualid` is added to the inheritance graph, new + coercion paths which have the same classes as existing ones are ignored. + The :cmd:`Coercion` command tries to check the convertibility of new ones and + existing ones. The paths for which this check fails are displayed by a warning + in the form :g:`[f₁;..;fₙ] : C >-> D`. + + The convertibility checking procedure for coercion paths is complete for + paths consisting of coercions satisfying the uniform inheritance condition, + but some coercion paths could be reported as ambiguous even if they are + convertible with existing ones when they have coercions that don't satisfy + the uniform inheritance condition. .. cmdv:: Local Coercion @qualid : @class >-> @class diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 2ba13db042..db3e20a9c6 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -470,7 +470,7 @@ Settings .. flag:: Typeclasses Dependency Order - This flag (on by default since 8.6) respects the dependency order + This flag (off by default) respects the dependency order between subgoals, meaning that subgoals on which other subgoals depend come first, while the non-dependent subgoals were put before the dependent ones previously (Coq 8.5 and below). This can result in diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index cc4976587d..1b9e3ce0f3 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -487,7 +487,7 @@ used as a convenient shorthand for abstractions, especially in local definitions or type expressions. Wildcards may be interpreted as abstractions (see for example sections -:ref:`definitions_ssr` and ref:`structure_ssr`), or their content can be +:ref:`definitions_ssr` and :ref:`structure_ssr`), or their content can be inferred from the whole context of the goal (see for example section :ref:`abbreviations_ssr`). @@ -983,13 +983,13 @@ During the course of a proof |Coq| always present the user with a Fk : Pk … ================= - forall (xl : Tl ) …, + forall (xl : Tl) …, let ym := bm in … in Pn -> … -> C The *goal* to be proved appears below the double line; above the line is the *context* of the sequent, a set of declarations of *constants* -``ci`` , *defined constants* d i , and *facts* ``Fk`` that can be used to +``ci`` , *defined constants* ``dj`` , and *facts* ``Fk`` that can be used to prove the goal (usually, ``Ti`` , ``Tj : Type`` and ``Pk : Prop``). The various kinds of declarations can come in any order. The top part of the @@ -1893,9 +1893,9 @@ under fresh |SSR| names. case E : a => H. Show 2. -Combining the generation of named equations mechanism with thecase +Combining the generation of named equations mechanism with the :tacn:`case` tactic strengthens the power of a case analysis. On the other hand, -when combined with the elim tactic, this feature is mostly useful for +when combined with the :tacn:`elim` tactic, this feature is mostly useful for debug purposes, to trace the values of decomposed parameters and pinpoint failing branches. @@ -2022,7 +2022,7 @@ be substituted. The equation always refers to the first :token:`d_item` in the actual tactic call, before any padding with initial ``_``. Thus, if an inductive type - has two family parameters, it is possible to have|SSR| generate an + has two family parameters, it is possible to have |SSR| generate an equation for the second one by omitting the pattern for the first; note however that this will fail if the type of the second parameter depends on the value of the first parameter. @@ -2320,7 +2320,7 @@ For instance, the tactic: tactic; do 1? rewrite mult_comm. rewrites at most one time the lemma ``mult_comm`` in all the subgoals -generated by tactic , whereas the tactic: +generated by tactic, whereas the tactic: .. coqdoc:: @@ -2511,7 +2511,7 @@ which behave like: have: term ; first by tactic. move=> clear_switch i_item. -Note that the :token:`clear_switch` *precedes* the:token:`i_item`, which +Note that the :token:`clear_switch` *precedes* the :token:`i_item`, which allows to reuse a name of the context, possibly used by the proof of the assumption, to introduce the new assumption itself. @@ -2783,7 +2783,7 @@ The + the order of the generated subgoals is inversed -+ but the optional clear item is still performed in the *second* ++ the optional clear item is still performed in the *second* branch. This means that the tactic: .. coqdoc:: @@ -2929,7 +2929,7 @@ facts. If an :token:`ident` is prefixed with the ``@`` mark, then a let-in redex is created, which keeps track if its body (if any). The syntax -``( ident := c_pattern)`` allows to generalize an arbitrary term using a +:n:`(@ident := @c_pattern)` allows to generalize an arbitrary term using a given name. Note that its simplest form ``(x := y)`` is just a renaming of ``y`` into ``x``. In particular, this can be useful in order to simulate the generalization of a section variable, otherwise not allowed. Indeed @@ -3917,7 +3917,7 @@ definitely want to avoid repeating large subterms of the goal in the proof script. We do this by “clamping down” selected function symbols in the goal, which prevents them from being considered in simplification or rewriting steps. This clamping is accomplished by -using the occurrence switches (see section:ref:`abbreviations_ssr`) +using the occurrence switches (see section :ref:`abbreviations_ssr`) together with “term tagging” operations. |SSR| provides two levels of tagging. @@ -4385,7 +4385,7 @@ Contextual patterns in rewrite Note: the simplification rule ``addSn`` is applied only under the ``f`` symbol. - Then we simplify also the first addition and expand 0 into 0+0. + Then we simplify also the first addition and expand ``0`` into ``0 + 0``. .. coqtop:: all @@ -4738,7 +4738,7 @@ Interpreting assumptions Interpreting an assumption in the context of a proof consists in applying to it a lemma before generalizing, and/or decomposing this assumption. For instance, with the extensive use of boolean reflection -(see section :ref:`views_and_reflection_ssr`.4), it is quite frequent +(see section :ref:`views_and_reflection_ssr`), it is quite frequent to need to decompose the logical interpretation of (the boolean expression of) a fact, rather than the fact itself. This can be achieved by a combination of ``move : _ => _`` switches, like in the @@ -5201,7 +5201,7 @@ There are three steps in the behavior of an assumption view tactic: For a ``case/term`` tactic, the generalisation step is replaced by a case analysis step. -*View hints* are declared by the user (see section:ref:`views_and_reflection_ssr`.8) and are +*View hints* are declared by the user (see section :ref:`views_and_reflection_ssr`) and are stored in the Hint View database. The proof engine automatically detects from the shape of the top assumption ``top`` and of the view lemma ``term`` provided to the tactic the appropriate view hint in the |