diff options
| author | Pierre-Marie Pédrot | 2018-10-23 09:49:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-23 09:49:32 +0200 |
| commit | dc3926c5ddcfe7596de37bb50a30bb3f492ea0d5 (patch) | |
| tree | 9d8a387082866bf25868845992194932180e5b30 /doc | |
| parent | 8b9b1be48a9c83f70cbfb70f52eabc616065fa1e (diff) | |
| parent | 057345df3a6f5e46b76b9d8a395d75ba8b0965e9 (diff) | |
Merge remote-tracking branch 'origin/pr/71'
Diffstat (limited to 'doc')
| -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 |