aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Courtieu2002-06-11 20:35:10 +0000
committerPierre Courtieu2002-06-11 20:35:10 +0000
commit18111fbde76762f2e6e02005741754b0967fdb4b (patch)
tree49ed89a504eabef01eb91bffee82ec42a37d670a
parent535d91629926249c335a17eddae24e1676c0cca0 (diff)
Not important.
-rw-r--r--CHANGES4
1 files changed, 2 insertions, 2 deletions
diff --git a/CHANGES b/CHANGES
index 26ce4c4c..a3f47cbe 100644
--- a/CHANGES
+++ b/CHANGES
@@ -69,8 +69,8 @@ contributed by Lucas Dixon (lucasd@dai.ed.ac.uk)
** Coq Changes
*** New Feature: There are some configurable variables that allow the
- user to register his own tactics and commands. Tactics and
- commands are split into backable (resp. undoable), i.e. which need
+ user to register his own tactics and commands. commands and
+ Tactics are split into backable (resp. undoable), i.e. which need
"Back" (resp. "Undo") to be backtracked and not backable
(resp. not undoable). We give an example of existing commands that
fit each category.