diff options
| author | Langston Barrett | 2018-08-07 11:35:50 -0700 |
|---|---|---|
| committer | Langston Barrett | 2018-08-07 11:35:50 -0700 |
| commit | 057345df3a6f5e46b76b9d8a395d75ba8b0965e9 (patch) | |
| tree | 17b4c65e14e3e2b1342d954065eefd3e2daa0ded | |
| parent | 888479b3514d714253d789d9ed054eaf422f5e14 (diff) | |
fix three small typos
| -rw-r--r-- | doc/ltac2.md | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/ltac2.md b/doc/ltac2.md index 9ba227c285..38cdef025e 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -17,7 +17,7 @@ Following the need of users that start developing huge projects relying critically on Ltac, we believe that we should offer a proper modern language that features at least the following: -- at least informal, predictible semantics +- at least informal, predictable semantics - a typing system - standard programming facilities (i.e. datatypes) @@ -388,7 +388,7 @@ represent several goals, including none. Thus, there is no such thing as It is natural to do the same in Ltac2, but we must provide a way to get access to a given goal. This is the role of the `enter` primitive, that applies a -tactic to each currently focussed goal in turn. +tactic to each currently focused goal in turn. ``` val enter : (unit -> unit) -> unit @@ -634,7 +634,7 @@ bindings, so that there will be a syntax error if one of the bound variables starts with an uppercase character. The semantics of this construction is otherwise the same as the corresponding -one from Ltac1, except that it requires the goal to be focussed. +one from Ltac1, except that it requires the goal to be focused. ## Match over goals |