diff options
Diffstat (limited to 'doc')
7 files changed, 87 insertions, 8 deletions
diff --git a/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst new file mode 100644 index 0000000000..055006d3b4 --- /dev/null +++ b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst @@ -0,0 +1,9 @@ +- **Changed:** + Tactic :tacn:`subst` :n:`@ident` now fails over a section variable which is + indirectly dependent in the goal; the incompatibility can generally + be fixed by first clearing the hypotheses causing an indirect + dependency, as reported by the error message, or by using :tacn:`rewrite` :n:`in *` + instead; similarly, :tacn:`subst` has no more effect on such variables + (`#12146 <https://github.com/coq/coq/pull/12146>`_, + by Hugo Herbelin; fixes `#10812 <https://github.com/coq/coq/pull/10812>`_; + fixes `#12139 <https://github.com/coq/coq/pull/12139>`_). diff --git a/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst b/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst new file mode 100644 index 0000000000..dc438f151e --- /dev/null +++ b/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Loss of location of some tactic errors + (`#12223 <https://github.com/coq/coq/pull/12223>`_, + by Hugo Herbelin; fixes + `#12152 <https://github.com/coq/coq/pull/12152>`_ and + `#12255 <https://github.com/coq/coq/pull/12255>`_). diff --git a/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst new file mode 100644 index 0000000000..0dd0fed4e2 --- /dev/null +++ b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst @@ -0,0 +1,6 @@ +- **Added:** + The Ltac2 rebinding command :cmd:`Ltac2 Set` has been extended with the ability to + give a name to the old value so as to be able to reuse it inside the + new one + (`#11503 <https://github.com/coq/coq/pull/11503>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/10-standard-library/12008-ollibs-bool.rst b/doc/changelog/10-standard-library/12008-ollibs-bool.rst index 7c10d261a7..42e5eb96eb 100644 --- a/doc/changelog/10-standard-library/12008-ollibs-bool.rst +++ b/doc/changelog/10-standard-library/12008-ollibs-bool.rst @@ -1,5 +1,5 @@ - **Added:** - Order relations ``ltb`` and ``compareb`` added in ``Bool.Bool``. + Order relations ``lt`` and ``compare`` added in ``Bool.Bool``. Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx`` (`#12008 <https://github.com/coq/coq/pull/12008>`_, by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12162-bool-leb.rst b/doc/changelog/10-standard-library/12162-bool-leb.rst new file mode 100644 index 0000000000..6a4070a82e --- /dev/null +++ b/doc/changelog/10-standard-library/12162-bool-leb.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + ``Bool.leb`` in favor of ``Bool.le``. The definition of ``Bool.le`` is made local to avoid conflicts with ``Nat.le``. As a consequence, previous calls to ``leb`` based on importing ``Bool`` should now be qualified into ``Bool.le`` even if ``Bool`` is imported. + (`#12162 <https://github.com/coq/coq/pull/12162>`_, + by Olivier Laurent). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 35062e0057..1e35160205 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -213,25 +213,63 @@ There is dedicated syntax for list and array literals. Ltac Definitions ~~~~~~~~~~~~~~~~ -.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_term +.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_value :name: Ltac2 This command defines a new global Ltac2 value. - For semantic reasons, the body of the Ltac2 definition must be a syntactical - value, that is, a function, a constant or a pure constructor recursively applied to - values. + The body of an Ltac2 definition is required to be a syntactical value + that is, a function, a constant, a pure constructor recursively applied to + values or a (non-recursive) let binding of a value in a value. + + .. productionlist:: coq + ltac2_value: fun `ltac2_var` => `ltac2_term` + : `ltac2_qualid` + : `ltac2_constructor` `ltac2_value` ... `ltac2_value` + : `ltac2_var` + : let `ltac2_var` := `ltac2_value` in `ltac2_value` If ``rec`` is set, the tactic is expanded into a recursive binding. If ``mutable`` is set, the definition can be redefined at a later stage (see below). -.. cmd:: Ltac2 Set @qualid := @ltac2_term +.. cmd:: Ltac2 Set @qualid {? as @lident} := @ltac2_term :name: Ltac2 Set This command redefines a previous ``mutable`` definition. Mutable definitions act like dynamic binding, i.e. at runtime, the last defined value for this entry is chosen. This is useful for global flags and the like. + The previous value of the binding can be optionally accessed using the `as` + binding syntax. + + .. example:: Dynamic nature of mutable cells + + .. coqtop:: all + + Ltac2 mutable x := true. + Ltac2 y := x. + Ltac2 Eval y. + Ltac2 Set x := false. + Ltac2 Eval y. + + .. example:: Interaction with recursive calls + + + .. coqtop:: all + + Ltac2 mutable rec f b := match b with true => 0 | _ => f true end. + Ltac2 Set f := fun b => + match b with true => 1 | _ => f true end. + Ltac2 Eval (f false). + Ltac2 Set f as oldf := fun b => + match b with true => 2 | _ => oldf false end. + Ltac2 Eval (f false). + + In the definition, the `f` in the body is resolved statically + because the definition is marked recursive. In the first re-definition, + the `f` in the body is resolved dynamically. This is witnessed by + the second re-definition. + Reduction ~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index bc2168411b..439f7fb9f6 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2832,6 +2832,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also unfolded and cleared. + If :n:`@ident` is a section variable it is expected to have no + indirect occurrences in the goal, i.e. that no global declarations + implicitly depending on the section variable must be present in the + goal. + .. note:: + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the first one is used. @@ -2845,9 +2850,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacv:: subst - This applies subst repeatedly from top to bottom to all identifiers of the + This applies :tacn:`subst` repeatedly from top to bottom to all hypotheses of the context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` - or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``. + or :n:`@ident := t` exists, with :n:`@ident` not occurring in + ``t`` and :n:`@ident` not a section variable with indirect + dependencies in the goal. .. flag:: Regular Subst Tactic @@ -2873,6 +2880,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. hypotheses, which without the flag it may break. default. + .. exn:: Cannot find any non-recursive equality over :n:`@ident`. + :undocumented: + + .. exn:: Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in hypothesis :n:`@ident`. + Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in the conclusion. + + Raised when the variable is a section variable with indirect + dependencies in the goal. + .. tacn:: stepl @term :name: stepl |