diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 3896446925..9812c45f7b 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -12,9 +12,11 @@ open Environ (*********************************************************************** s Reduction functions *) +(* None of these functions do eta reduction *) + val whd_betaiotazeta : env -> constr -> constr -val whd_betadeltaiota : env -> constr -> constr -val whd_betadeltaiota_nolet : env -> constr -> constr +val whd_all : env -> constr -> constr +val whd_allnolet : env -> constr -> constr val whd_betaiota : env -> constr -> constr val nf_betaiota : env -> constr -> constr |