diff options
| author | Jasper Hugunin | 2018-01-17 15:03:25 +0900 |
|---|---|---|
| committer | Jasper Hugunin | 2018-01-17 15:03:25 +0900 |
| commit | d8652efca406c852ebc27cb27c903d9a6a4b2532 (patch) | |
| tree | 9f76056d7fee478320eb035d62db25bb5f570192 | |
| parent | 2d8dcd741d229c4de57ccce9f3ab09b808ccfc94 (diff) | |
Add CHANGES entry
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -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 |
