diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 13 |
1 files changed, 13 insertions, 0 deletions
@@ -40,6 +40,14 @@ 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 tactics "dtauto", "dintuition", "firstorder" now handle inductive types + with let bindings in the parameters. + +Focusing + +- Focusing bracket `{` now supports single-numbered goal selector, + e.g. `2: {` will focus on the second sub-goal. As usual, unfocus + with `}` once the sub-goal is fully solved. Vernacular Commands @@ -60,6 +68,11 @@ Checker - The checker now accepts filenames in addition to logical paths. +CoqIDE + +- Find and Replace All report the number of occurrences found; Find indicates + when it wraps. + Documentation - The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been |