diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-19 16:24:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-19 16:24:42 +0000 |
| commit | b41a1cd0edd2fc4a0da2a04f10554a4737a5c192 (patch) | |
| tree | 008ab9b03f94363059cf7e3a3fe80572277d8bdf /toplevel | |
| parent | 802c757f5bbd7201e5aaccb0eb777c2702594b55 (diff) | |
correction de bugs sur commit précédent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1156 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/record.ml | 10 |
1 files 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 |