diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 0 insertions, 3 deletions
@@ -62,9 +62,6 @@ Vernacular commands Coq: terms, modules, tactics, etc. The old behavior of the command can be retrieved using the "Locate Term" command. - New "Derive" command to help writing program by derivation. -- "Undo" undoes any command, not just tactics. -- "Undo. Undo." does not work in CoqIDE or Proof General, it works only - in coqtop. "Undo 2" should be used intead. - New "Refine Instance Mode" option that allows to deactivate the generation of obligations in incomplete typeclass instances, raising an error instead. - "Collection" command to name sets of section hypotheses. Named collections |