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 a47b19242f..ae0640aef0 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -200,6 +200,7 @@ val whd_ise1 : 'a evar_map -> constr -> constr val nf_ise1 : 'a evar_map -> constr -> constr exception Uninstantiated_evar of int val whd_ise : 'a evar_map -> constr -> constr +val whd_castappevar : 'a evar_map -> constr -> constr (*s Obsolete Reduction Functions *) |