aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJasper Hugunin2018-01-17 15:03:25 +0900
committerJasper Hugunin2018-01-17 15:03:25 +0900
commitd8652efca406c852ebc27cb27c903d9a6a4b2532 (patch)
tree9f76056d7fee478320eb035d62db25bb5f570192
parent2d8dcd741d229c4de57ccce9f3ab09b808ccfc94 (diff)
Add CHANGES entry
-rw-r--r--CHANGES2
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index ead751147a..d91181a1d4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -40,6 +40,8 @@ Tactics
- Added tactic optimize_heap, analogous to the Vernacular Optimize
Heap, which performs a major garbage collection and heap compaction
in the OCaml run-time system.
+- The tactic "dtauto" now handles some inductives such as
+ "@sigT A (fun _ => B)" as non-dependent conjunctions.
Vernacular Commands