diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-13 18:59:59 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-13 18:59:59 +0000 |
| commit | cdb783158991ab7139e55f8a2e85d409e1ac8493 (patch) | |
| tree | a901235166bdbbdfd69df0d2bc20e32814a47a96 | |
| parent | 8d8abed37c87368c2bdb8adde09bc8b69a408787 (diff) | |
Fix a bug, in fold_constr_with_binders, the types of fixpoints were
processed in the larger context instead of the bodies.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11400 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/termops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index f0a781cf0..654cd2b1a 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -425,11 +425,11 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with | Fix (_,(lna,tl,bl)) -> let n' = iterate g (Array.length tl) n in let fd = array_map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> let n' = iterate g (Array.length tl) n in let fd = array_map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate subterms of [c]; it carries an extra data [acc] which is processed by [g] at |