diff options
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index a0281fa50b..fcb52cf275 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -207,7 +207,7 @@ Applying theorems or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many subgoals as there are holes in the term. The type of holes must be either synthesized by the system or declared by an explicit cast - like ``(_ : nat->Prop)``. Any subgoal that + like ``(_ : nat -> Prop)``. Any subgoal that occurs in other subgoals is automatically shelved, as if calling :tacn:`shelve_unifiable`. This low-level tactic can be useful to advanced users. @@ -680,14 +680,14 @@ Managing the local context .. example:: - On the subgoal :g:`forall x y : nat, x=y -> y=x` the + On the subgoal :g:`forall x y : nat, x = y -> y = x` the tactic :n:`intros until 1` is equivalent to :n:`intros x y H`, - as :g:`x=y -> y=x` is the first non-dependent product. + as :g:`x = y -> y = x` is the first non-dependent product. - On the subgoal :g:`forall x y z:nat, x=y -> y=x` the + On the subgoal :g:`forall x y z : nat, x = y -> y = x` the tactic :n:`intros until 1` is equivalent to :n:`intros x y z` as the product on :g:`z` can be rewritten as a non-dependent - product: :g:`forall x y:nat, nat -> x=y -> y=x`. + product: :g:`forall x y : nat, nat -> x = y -> y = x`. .. exn:: No such hypothesis in current goal. |