aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorArnaud Spiwack2014-07-25 15:17:28 +0200
committerArnaud Spiwack2014-07-25 19:06:22 +0200
commit6f7aebb09c89e95bd7520dad482f20e7a11fb279 (patch)
tree6b8160cdb1c9174fba670bb1189391ef39a69983
parent3c517ad28894297f822c850ad75a1c0f09b60536 (diff)
CHANGE: add Derive.
-rw-r--r--CHANGES1
1 files changed, 1 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index c20f4ca894..de2f0948cd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -55,6 +55,7 @@ Vernacular commands
- The "Locate" command now searches through all sorts of qualified namespaces of
Coq: terms, modules, tactics, etc. The old behaviour of the command can be
retrieved using the "Locate Term" command.
+- New "Derive" command to help writing program by derivation.
Specification Language