Passage à une représentation des fixpoints plus primitive dans constr_expr (càd avec indices)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3245 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 5 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2ce1a4db0..e760f3e92 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -293,12 +293,9 @@ let rec intern_cases_pattern scopes aliases = function
 
 let rec intern_fix = function
   | [] -> ([],[],[],[])
-  | (fi, bl, c, t)::rest->
-      let ni = List.length (List.flatten (List.map fst bl)) - 1 in
+  | (fi, n, c, t)::rest->
       let (lf,ln,lc,lt) = intern_fix rest in
-      (fi::lf, ni::ln, 
-       CProdN (dummy_loc, bl, c)::lc, 
-       CLambdaN (dummy_loc, bl, t)::lt)
+      (fi::lf, n::ln, c::lc, t::lt)
 
 let rec intern_cofix = function
   | [] -> ([],[],[])