diff options
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 dd0a81603c..4ce1338443 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -48,6 +48,9 @@ Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta +In intf/genredexpr.mli, fIota was replaced by FMatch, FFix and +FCofix. Similarly, rIota was replaced by rMatch, rFix and rCofix. + ** Notation_ops ** Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr. |