diff options
| author | Enrico Tassi | 2016-06-17 16:26:59 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-17 16:27:35 +0200 |
| commit | 8a45a3a5d08f9e9339d0ba9cc9624a895d4cfc57 (patch) | |
| tree | 84d49919537123dd73464899cbfbe0e0a5f069ba | |
| parent | 57a3f38832dba3a9b7a1de146bd45451227a03e8 (diff) | |
Mentioning goal selectors in CHANGES
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -28,6 +28,8 @@ Tactics a locally free identifier anymore. It must use e.g. the "fresh" primitive instead (potential source of incompatibilities). - New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac (DOC TODO). +- New goal selectors. Sets of goals can be selected by select by listing + integers ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24. Hints |