diff options
| author | JPR | 2019-05-21 23:07:55 +0200 |
|---|---|---|
| committer | JPR | 2019-05-21 23:07:55 +0200 |
| commit | e6322e23958a937fa01960f8ce320717b9863253 (patch) | |
| tree | 79e2a8c8e7c953c44b3880fa683d82f2a6e6cc85 /dev/doc/changes.md | |
| parent | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (diff) | |
Fixing typos - Part 1
Diffstat (limited to 'dev/doc/changes.md')
| -rw-r--r-- | dev/doc/changes.md | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 7221c3de56..339ac2d9b7 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1278,7 +1278,7 @@ next_global_ident_away true -> next_ident_away_in_goal next_global_ident_away false -> next_global_ident_away ``` -### Cleaning in commmand.ml +### Cleaning in command.ml Functions about starting/ending a lemma are in lemmas.ml Functions about inductive schemes are in indschemes.ml @@ -1593,7 +1593,7 @@ Other kinds of objects: #### Writing subst_thing functions -The subst_thing shoud not copy the thing if it hasn't actually +The subst_thing should not copy the thing if it hasn't actually changed. There are some cool emacs macros in dev/objects.el to help writing subst functions this way quickly and without errors. Also there are *_smartmap functions in Util. |