From accde4d40c89f0a40caacb9e91db61f204b05918 Mon Sep 17 00:00:00 2001
From: Thomas Sibut-Pinote
Date: Tue, 23 Jun 2015 19:10:25 +0200
Subject: 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.
---
 dev/doc/changes.txt | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'dev')

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
-- 
cgit v1.2.3