diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 7bb43b0556..362fbcfc8c 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -210,8 +210,6 @@ val nf_ise1 : 'a evar_map -> constr -> constr exception Uninstantiated_evar of int val whd_ise : 'a evar_map -> constr -> constr -val whd_ise1_metas : 'a evar_map -> constr -> constr - (*s Obsolete Reduction Functions *) (*i |