diff options
| author | Pierre-Marie Pédrot | 2020-05-12 17:13:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-12 17:13:05 +0200 |
| commit | efb78e3c413bcc66d470ba4046c56bae0a61f56f (patch) | |
| tree | a2139fd2681c93563a1272c4d545931ad7b6485b /doc/sphinx/proof-engine | |
| parent | 697730186f17ac3992b9b7966c505b8f64eab69d (diff) | |
| parent | 3a8376b5dc39e9b546470509b80de3fe9881c7f3 (diff) | |
Merge PR #12146: Fixes #10812: tactic subst failure with section variables indirectly dependent in goal
Ack-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 20 |
1 files changed, 18 insertions, 2 deletions
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 |