diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-01-08 16:59:47 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-01-08 16:59:57 +0100 |
| commit | b92fff621cce1576c93fab9276fb41ea85e10982 (patch) | |
| tree | d6e0c1964b274c9b00339452d77468f48ebe2794 /CHANGES | |
| parent | 448bf4529c5766e98367345076d00e64e25db7bf (diff) | |
Fixed and extend bullet related info/error messages. + doc.
Had to put some hook in the handler of Proofview.NoSuchgoals.
Documentation updated. CHANGE updated.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -224,6 +224,7 @@ Tactics so that terms with holes can be constructed piecewise in Ltac. - New bullets --, ++, **, ---, +++, ***, ... made available. - More informative messages when wrong bullet is used. +- bullet suggestion when a subgoal is solved. - New tactic "enough", symmetric to "assert", but with subgoals swapped, as a more friendly replacement of "cut". - In destruct/induction, experimental modifier "!" prefixing the |