diff options
| author | Hugo Herbelin | 2015-12-15 20:14:07 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-01-12 22:17:03 +0100 |
| commit | 74d89e0be05e5cb4c9faf154478bc0c907bec2bb (patch) | |
| tree | b4b73752b6060c5e1fe88304797c59aba87901ec | |
| parent | fc642ca962dd5228a5a714b8e41506dcbc3b6520 (diff) | |
Reporting about the new tactical unshelve.
| -rw-r--r-- | CHANGES | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -22,9 +22,11 @@ Tactics introducing along pattern p changed to p%c1..%cn. The feature and syntax are in experimental stage. - "Proof using" does not clear unused section variables. -- "refine" has been changed back to the 8.4 behavior of shelving subgoals - that occur in other subgoals. The "refine" tactic of 8.5beta2 has been +- Tactic "refine" has been changed back to the 8.4 behavior of shelving subgoals + that occur in other subgoals. The "refine" tactic of 8.5beta3 has been renamed "simple refine"; it does not shelve any subgoal. +- New tactical "unshelve tac" which grab existential variables put on + the tactic shelve by the execution of "tac". Changes from V8.5beta2 to V8.5beta3 =================================== @@ -495,11 +497,9 @@ Interfaces documentation of OCaml's Str module for the supported syntax. - Many CoqIDE windows, including the query one, are now detachable to improve usability on multi screen work stations. - - Coqtop/coqc outputs highlighted syntax. Colors can be configured thanks to the COQ_COLORS environment variable, and their current state can be displayed with the -list-tags command line option. - - Third party user interfaces can install their main loop in $COQLIB/toploop and call coqtop with the -toploop flag to select it. |