diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index a6ebda4918..ced0fd3413 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -17,6 +17,7 @@ val whd_betaiotazeta : constr -> constr val whd_betadeltaiota : env -> constr -> constr val whd_betadeltaiota_nolet : env -> constr -> constr +val whd_betaiota : constr -> constr val nf_betaiota : constr -> constr (*********************************************************************** |