diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-15 16:59:37 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-15 16:59:57 +0100 |
| commit | 8cee2c7ef9e15937fafe60ae43fec7c8bb3678c6 (patch) | |
| tree | 341d2ada067944e77768e3da7afded1142525b0b | |
| parent | 362b7ef4422b451e621ca8400692de1decb0503d (diff) | |
Note about "Undo. Undo." in CHANGES
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -63,6 +63,8 @@ Vernacular commands 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 |