diff options
| author | Maxime Dénès | 2017-08-17 16:38:30 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-17 16:38:30 +0200 |
| commit | 63da901edc3ab5b69098499cdc01ab50ed9b3353 (patch) | |
| tree | 0f1c411b9621416ef2720b81430508b619523ff9 /dev | |
| parent | 7451651a70be86ef8f510faabcba445766595187 (diff) | |
| parent | 6de02170275e49e5f58a93eb5513d5eb8cb9aa38 (diff) | |
Merge PR #972: 8.7 change entries
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index a48c491d33..0f1a28028c 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -188,6 +188,9 @@ In Coqlib / reference location: - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase was very specific. Use tclPROGRESS instead. +- New (internal) tactical `tclINDEPENDENTL` that combined with enter_one allows + to iterate a non-unit tactic on all goals and access their returned values. + - The unsafe flag of the Refine.refine function and its variants has been renamed and dualized into typecheck and has been made mandatory. |