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 /kernel/reduction.mli | |
| 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
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 |