diff options
| author | Thomas Sibut-Pinote | 2015-06-23 19:10:25 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-06-04 19:45:25 +0200 |
| commit | accde4d40c89f0a40caacb9e91db61f204b05918 (patch) | |
| tree | e7a48a6f42a1ca53c0aa10e3de67fe1846fd6c48 /dev/doc | |
| parent | b91f5d1adbd039809e31b5311d06b376829de1fc (diff) | |
Added support for a side effect on constants in reduction functions.
This exports two functions:
- declare_reduction_effect: to declare a hook to be applied when some
constant are visited during the execution of some reduction functions
(primarily cbv, but also cbn, simpl, hnf, ...).
- set_reduction_effect: to declare a constant on which a given effect
hook should be called.
Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin.
Added support for printing effect in functions of tacred.ml.
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.txt | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index bcda4ff50a..631b5f5aaf 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -10,6 +10,16 @@ will fail to compile now. They should switch to `Bytes.t` * ML API * +Added two functions for declaring hooks to be executed in reduction +functions when some given constants are traversed: + + declare_reduction_effect: to declare a hook to be applied when some + constant are visited during the execution of some reduction functions + (primarily cbv). + + set_reduction_effect: to declare a constant on which a given effect + hook should be called. + We renamed the following functions: Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr |