Bug factorisation

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

1 files changed, 6 insertions, 6 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 0574945977..bd31a78b4c 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -25,17 +25,17 @@ let split_lambda = function
   | _ -> Util.error "ill-formed fixpoint body"
 
 let split_product = function
-  | CArrow (loc,t,c) -> c
-  | CProdN (loc,[[na],t],c) -> c
-  | CProdN (loc,([na],t)::bl,c) -> CProdN(loc,bl,c)
-  | CProdN (loc,(na::nal,t)::bl,c) -> CProdN(loc,(nal,t)::bl,c)
+  | CArrow (loc,t,c) -> ((loc,Anonymous),t,c)
+  | CProdN (loc,[[na],t],c) -> (na,t,c)
+  | CProdN (loc,([na],t)::bl,c) -> (na,t,CProdN(loc,bl,c))
+  | CProdN (loc,(na::nal,t)::bl,c) -> (na,t,CProdN(loc,(nal,t)::bl,c))
   | _ -> Util.error "ill-formed fixpoint body"
 
 let rec split_fix n typ def =
   if n = 0 then ([],typ,def)
   else
-    let (na,t,def) = split_lambda def in
-    let typ = split_product typ in
+    let (na,_,def) = split_lambda def in
+    let (_,t,typ) = split_product typ in
     let (bl,typ,def) = split_fix (n-1) typ def in
     (([na],t)::bl,typ,def)