Commit cd10f5a6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix typos.

parent f42d7b3e
Pipeline #3935 passed with stage
in 3 minutes and 57 seconds
...@@ -124,8 +124,8 @@ The later modality ...@@ -124,8 +124,8 @@ The later modality
- `iNext n` : introduce `n` laters by stripping that number of laters from all - `iNext n` : introduce `n` laters by stripping that number of laters from all
hypotheses. If the argument `n` is not given, it strips one later if the hypotheses. If the argument `n` is not given, it strips one later if the
leftmost conjuct is of the shape `▷ P`, or `n` laters if the leftmost conjuct leftmost conjunct is of the shape `▷ P`, or `n` laters if the leftmost
is of the shape `▷^n P`. conjunct is of the shape `▷^n P`.
- `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by - `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by
generating a hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq generating a hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq
level variables `x1 ... xn`, the hypotheses given by the selection pattern level variables `x1 ... xn`, the hypotheses given by the selection pattern
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment