diff options
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. |