diff options
| author | Théo Zimmermann | 2018-08-01 12:40:21 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-08-22 10:49:01 +0200 |
| commit | ed76ae4246e7d8fca79944b12b058d6bc3cd702b (patch) | |
| tree | f1d7c5a0ae7cb539a2bc69aaced640145104debd | |
| parent | 30644a4e88f3fd0f0fc2ced117e38c9aa59affc5 (diff) | |
[refman] Fixing two nested lemma errors.
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index d55748d645..35c974e2e1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -974,7 +974,7 @@ Managing the local context .. example:: - .. coqtop:: all + .. coqtop:: reset all Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. intros x H z y H0. @@ -1098,7 +1098,7 @@ Managing the local context .. example:: - .. coqtop:: all + .. coqtop:: reset all Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C. intros A B C H; decompose [and or] H. |