diff options
| -rw-r--r-- | kernel/reduction.ml | 14 | ||||
| -rw-r--r-- | kernel/reduction.mli | 2 |
2 files changed, 0 insertions, 16 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 0e47053c62..ad1ac931e8 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1194,17 +1194,3 @@ let nf_ise1 sigma = strong (fun _ -> whd_ise1) empty_env sigma (* A form of [whd_ise1] with type "reduction_function" *) let whd_evar env = whd_ise1 - -(* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables - * Similarly we have is_fmachine1_metas and is_resolve1_metas *) - -let rec whd_ise1_metas sigma t = - let t' = strip_outer_cast t in - match kind_of_term t' with - | IsEvar (ev,args as k) when Evd.in_dom sigma ev -> - if Evd.is_defined sigma ev then - whd_ise1_metas sigma (existential_value sigma k) - else - mkCast (mkMeta (new_meta()), existential_type sigma k) - | _ -> t' - 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 |