diff options
| -rw-r--r-- | doc/PG-adapting.texi | 2 | ||||
| -rw-r--r-- | generic/proof-shell.el | 2 | ||||
| -rw-r--r-- | generic/proof-tree.el | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 0c62973d..d5264412 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -2882,7 +2882,7 @@ editing mode. The other variables are only used when the proof shell is running. They can therefore be configured with the -proof-assistent proof-shell mode. +proof assistant proof-shell mode. @node Prooftree Adaption diff --git a/generic/proof-shell.el b/generic/proof-shell.el index c889b789..49107ff2 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1032,7 +1032,7 @@ contains only invisible elements for Prooftree synchronization." ;; This is the point where old items have been removed from ;; proof-action-list and where the next item has not yet been - ;; sent to the proof assistent. This is therefore one of the + ;; sent to the proof assistant. This is therefore one of the ;; few points where it is safe to manipulate ;; proof-action-list. The urgent proof-tree display actions ;; must therefore be called here, because they might add some diff --git a/generic/proof-tree.el b/generic/proof-tree.el index 1f4bd208..6a34d919 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -272,7 +272,7 @@ function should return nil and prooftree will not get updated." "Proof assistant specific function for the start of the current proof. This function is called with no argument when the user switches the external proof-tree display on. Then, this function must -determin if there is a currently unfinished proof for which the +determine if there is a currently unfinished proof for which the proof-tree display should be started. If yes this function must return the starting position of the command that started this proof. If there is no such proof, this function must return nil." |