diff options
| author | filliatr | 2001-04-11 07:56:19 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-11 07:56:19 +0000 |
| commit | 8a7452976731275212f0c464385b380e2d590f5e (patch) | |
| tree | 966ccb9cc83c2c38dcec9b7456b6adde3f8da7a4 /kernel | |
| parent | f88abe3e8012ab271ef09de5761d70fcad103d56 (diff) | |
réparation d'un bug de Correctness: whd_programs ne doit pas réduire les terms contenant des Evar pas des Metas; mise à jour des exemples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1577 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 72f577a7cc..aa60bfb8c5 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1007,7 +1007,7 @@ let rec apprec env sigma s = let hnf env sigma c = apprec env sigma (c, empty_stack) (* A reduction function like whd_betaiota but which keeps casts - * and does not reduce redexes containing meta-variables. + * and does not reduce redexes containing existential variables. * Used in Correctness. * Added by JCF, 29/1/98. *) @@ -1017,7 +1017,7 @@ let whd_programs_stack env sigma = | IsApp (f,cl) -> let n = Array.length cl - 1 in let c = cl.(n) in - if occur_meta c then + if occur_existential c then s else whrec (mkApp (f, Array.sub cl 0 n), append_stack [|c|] stack) @@ -1026,7 +1026,7 @@ let whd_programs_stack env sigma = | None -> s | Some (a,m) -> stacklam whrec [a] c m) | IsMutCase (ci,p,d,lf) -> - if occur_meta d then + if occur_existential d then s else let (c,cargs) = whrec (d, empty_stack) in |