diff options
| author | Vincent Laporte | 2018-10-24 11:42:01 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-24 11:54:31 +0000 |
| commit | bcf64b062a1dde1e2322e84cb041607bf76b0b78 (patch) | |
| tree | 8cecbaea107911d76e8ea971bab1b03c59ef3995 | |
| parent | a546d298a32e5000ef3f318b68924648adf1eb8a (diff) | |
[Manual] Avoid using deprecated “Focus”
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index bcef988874..6fde52f95e 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2486,8 +2486,7 @@ destruction of existential assumptions like in the tactic: .. coqtop:: all Lemma test : True. - have [x Px]: exists x : nat, x > 0. - Focus 2. + have [x Px]: exists x : nat, x > 0; last first. An alternative use of the ``have`` tactic is to provide the explicit proof term for the intermediate lemma, using tactics of the form: @@ -2565,8 +2564,7 @@ copying the goal itself. .. coqtop:: all Lemma test : True. - have suff H : 2 + 2 = 3. - Focus 2. + have suff H : 2 + 2 = 3; last first. Note that H is introduced in the second goal. @@ -2853,8 +2851,7 @@ pattern will be used to process its instance. .. coqtop:: all Lemma simple n (ngt0 : 0 < n ) : P n. - gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0). - Focus 2. + gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0); last first. .. _advanced_generalization_ssr: |