From 1d0a146fdf6642422a3409a820b18fc81bbfeeb8 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 14 Nov 2002 21:01:32 +0000 Subject: Bug factorisation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3239 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_constr.ml4 | 12 ++++++------ 1 file 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) -- cgit v1.2.3