diff options
| author |  Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr> | 2015-06-23 19:10:25 +0200 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-06-04 19:45:25 +0200 |
| commit | accde4d40c89f0a40caacb9e91db61f204b05918 (patch) | |
| tree | e7a48a6f42a1ca53c0aa10e3de67fe1846fd6c48 /kernel/cClosure.mli | |
| 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 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 077756ac7..69a5e79b4 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 |