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.
---
 kernel/cClosure.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 077756ac74..69a5e79b45 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -187,7 +187,7 @@ val create_clos_infos :
   ?evars:(existential->constr option) -> reds -> env -> clos_infos
 val oracle_of_infos : clos_infos -> Conv_oracle.oracle
 
-val env_of_infos : clos_infos -> env
+val env_of_infos : 'a infos -> env
 
 val infos_with_reds : clos_infos -> reds -> clos_infos
 
-- 
cgit v1.2.3