diff options
| author | herbelin | 2000-09-26 16:49:56 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-26 16:49:56 +0000 |
| commit | 1ae7bc6dfcd16ef4744c9648d836155bd4cded45 (patch) | |
| tree | 3d012f0a64fb52a40275fb311af4a2ce4fe04618 | |
| parent | a5de858fb3d47082124edfa8e421b8c80c41c7e2 (diff) | |
Retrait de whd_ise1_metas
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@616 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |