From cdb783158991ab7139e55f8a2e85d409e1ac8493 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 13 Sep 2008 18:59:59 +0000
Subject: 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
---
 pretyping/termops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f0a781cf0b..654cd2b1ae 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
-- 
cgit v1.2.3