From ab4f34c860fcd5b5362ea96097fbd51fbbf3f99a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 16 Nov 2002 22:55:16 +0000
Subject: Complétion du commit précédent

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3247 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6d1c1b145e..6bcc2433dd 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1603,7 +1603,7 @@ let cvt_fixpoint_binder = function
   | [],c -> xlate_error "Shouldn't occur"
 
 let cvt_fixpoint_binders bl =
-  CT_binder_list(List.map cvt_fixpoint_binder args)
+  CT_binder_list(List.map cvt_fixpoint_binder bl)
 
 let xlate_vernac =
  function
@@ -1873,9 +1873,9 @@ let xlate_vernac =
    | VernacFixpoint [] -> xlate_error "mutual recursive"
    | VernacFixpoint (lm :: lmi) ->
       let strip_mutrec (fid, n, arf, ardef) =
+        let (bl,arf,ardef) = Ppconstr.split_fix n arf ardef in
         let arf = xlate_constr arf in
         let ardef = xlate_constr ardef in
-        let (bl,arf,ardef) = split_fix n arf ardef in
 	match cvt_fixpoint_binders bl with
 	  | CT_binder_list (b :: bl) ->
 	      CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
-- 
cgit v1.2.3