diff options
Diffstat (limited to 'dev/doc/changes.txt')
| -rw-r--r-- | dev/doc/changes.txt | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 57c7a97d58..0f1a28028c 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -18,6 +18,10 @@ We changed the type of the following functions: The returned term contains De Bruijn universe variables. - Global.body_of_constant: same as above. +We renamed the following datatypes: + + Pp.std_ppcmds -> Pp.t + ========================================= = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = ========================================= @@ -184,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. |