From b41a1cd0edd2fc4a0da2a04f10554a4737a5c192 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 19 Dec 2000 16:24:42 +0000 Subject: correction de bugs sur commit précédent MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1156 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/record.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/toplevel/record.ml b/toplevel/record.ml index 19e399bab..826732c24 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -91,14 +91,14 @@ let warning_or_error coe st = pPNL (hOV 0 [< 'sTR"Warning: "; st >]) (* We build projections *) -let declare_projections idstruc coers params constr_types = +let declare_projections idstruc coers params fields = let r = global_reference CCI idstruc in - let lp = List.length constr_types in + let lp = List.length params in let rp1 = applist (r,(rel_list 0 lp)) in let rp2 = applist (r,(rel_list 1 lp)) in let x = Environ.named_hd (Global.env()) r Anonymous in let args = (* Rel 1 refers to "x" *) - (List.map (fun (id,_) -> mkVar id) constr_types)@[mkRel 1] in + (List.map (fun (id,_) -> mkVar id) params)@[mkRel 1] in let (sp_projs,_,_) = List.fold_left2 (fun (sp_projs,ids_not_ok,subst) coe (fi,ti) -> @@ -115,7 +115,7 @@ let declare_projections idstruc coers params constr_types = (None::sp_projs,fi::ids_not_ok,subst) end else let p = mkLambda (x, rp2, replace_vars subst ti) in - let branch = mk_LambdaCit constr_types (mkVar fi) in + let branch = mk_LambdaCit fields (mkVar fi) in let ci = Inductive.make_case_info (Global.lookup_mind_specif (destMutInd r)) (Some PrintLet) [| RegularPat |] in @@ -146,7 +146,7 @@ let declare_projections idstruc coers params constr_types = in (Some(path_of_const constr_fi)::sp_projs, ids_not_ok, (fi,constr_fip)::subst) end) - ([],[],[]) coers constr_types + ([],[],[]) coers fields in sp_projs (* Fields have names [idfs] and types [tyfs]; [coers] is a boolean list -- cgit v1.2.3