diff options
-rw-r--r-- | toplevel/record.ml | 28 | ||||
-rw-r--r-- | toplevel/record.mli | 2 |
2 files changed, 16 insertions, 14 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index c05220989..f6d8b6000 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -152,13 +152,14 @@ let declare_projections indsp coers fields = let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) let x = Termops.named_hd (Global.env()) r Anonymous in let lifted_fields = lift_rel_context 1 fields in - let (_,sp_projs,_) = + let (_,kinds,sp_projs,_) = List.fold_left2 - (fun (nfi,sp_projs,subst) coe (fi,optci,ti) -> - match fi with - | Anonymous -> - (nfi-1, None::sp_projs,NoProjection fi::subst) - | Name fid -> + (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) -> + let (sp_projs,subst) = + match fi with + | Anonymous -> + (None::sp_projs,NoProjection fi::subst) + | Name fid -> try let ccl = subst_projection fid subst ti in let body = match optci with @@ -192,17 +193,18 @@ let declare_projections indsp coers fields = let refi = ConstRef kn in let constr_fi = mkConst kn in if coe then begin - let cl = Class.class_of_ref (IndRef indsp) in + let cl = Class.class_of_global (IndRef indsp) in Class.try_add_new_coercion_with_source refi Global cl end; let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in let constr_fip = applist (constr_fi,proj_args) in - (nfi-1, (Some kn)::sp_projs, Projection constr_fip::subst) + (Some kn::sp_projs, Projection constr_fip::subst) with NotDefinable why -> warning_or_error coe indsp why; - (nfi-1, None::sp_projs,NoProjection fi::subst)) - (List.length fields,[],[]) coers (List.rev fields) - in sp_projs + (None::sp_projs,NoProjection fi::subst) in + (nfi-1,(optci=None)::kinds,sp_projs,subst)) + (List.length fields,[],[],[]) coers (List.rev fields) + in (kinds,sp_projs) (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean list telling if the corresponding fields must me declared as coercion *) @@ -232,7 +234,7 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) = mind_entry_inds = [mie_ind] } in let sp = declare_mutual_with_eliminations true mie in let rsp = (sp,0) in (* This is ind path of idstruc *) - let sp_projs = declare_projections rsp coers fields in + let kinds,sp_projs = declare_projections rsp coers fields in let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *) if is_coe then Class.try_add_new_coercion build Global; - Recordops.add_new_struc (rsp,idbuild,nparams,List.rev sp_projs) + Recordops.declare_structure(rsp,idbuild,nparams,List.rev kinds,List.rev sp_projs) diff --git a/toplevel/record.mli b/toplevel/record.mli index b8a1a6ce6..5074719bc 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -21,7 +21,7 @@ open Topconstr [coers]; it returns the absolute names of projections *) val declare_projections : - inductive -> bool list -> rel_context -> constant option list + inductive -> bool list -> rel_context -> bool list * constant option list val definition_structure : lident with_coercion * local_binder list * |