diff options
author | 2015-06-23 19:10:25 +0200 | |
---|---|---|
committer | 2017-06-04 19:45:25 +0200 | |
commit | accde4d40c89f0a40caacb9e91db61f204b05918 (patch) | |
tree | e7a48a6f42a1ca53c0aa10e3de67fe1846fd6c48 /theories/.dir-locals.el | |
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 'theories/.dir-locals.el')
0 files changed, 0 insertions, 0 deletions