aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/reduction.mli
diff options
context:
space:
mode:
Diffstat (limited to 'checker/reduction.mli')
-rw-r--r--checker/reduction.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 049bbad9b..0ca5f8368 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -14,7 +14,7 @@ open Environ
(************************************************************************)
(*s Reduction functions *)
-val whd_betaiotazeta : env -> constr -> constr
+val whd_betaiotazeta : constr -> constr
val whd_betadeltaiota : env -> constr -> constr
val whd_betadeltaiota_nolet : env -> constr -> constr