aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/closure.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 3d8fb71f3e..e401679181 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -50,6 +50,7 @@ val no_red : reds
val beta_red : reds
val betaiota_red : reds
val betadeltaiota_red : reds
+val betaiotazeta_red : reds
val unfold_red : evaluable_global_reference -> reds
(* Tests if a reduction kind is set *)