From e537a3deafdb8d2d4cebbcb592add25b93972540 Mon Sep 17 00:00:00 2001
From: bertot
Date: Thu, 22 Jan 2004 11:32:18 +0000
Subject: corrects the way the structural argument declaration is handled in
 fixpoint definitions

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

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index aae7d714f9..9c91d930eb 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -292,10 +292,15 @@ let rec decompose_last = function
   | a::tl -> let rl, b = decompose_last tl in (a::rl), b;;
 
 let rec make_fix_struct b = function
-    0, CProdN(_, [([na],_)], CProdN(_, _,_)) -> xlate_id_opt na
+    0, CProdN(_, [(na::tl,_)], CProdN(_, _,_)) -> xlate_id_opt na
   | 0, CProdN(_, [([na],_)], _) ->
       if b then xlate_id_opt na else ctv_ID_OPT_NONE
-  | n, CProdN(_, [([_],_)],body) -> make_fix_struct true ((n-1),body)
+  | n, CProdN(_, [(l,_)],body) -> 
+      let len = List.length l in
+	if len <= n then
+	  make_fix_struct true (n-len, body)
+	else
+	  xlate_id_opt(List.nth l n)
   | _, _ -> xlate_error "unexpected result of parsing for Fixpoint";;
 
 
-- 
cgit v1.2.3