diff options
| -rw-r--r-- | pretyping/recordops.ml | 21 | ||||
| -rw-r--r-- | pretyping/recordops.mli | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
3 files changed, 12 insertions, 13 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 81cbd0213b..08924d0320 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -45,14 +45,14 @@ let structure_table = let projection_table = Summary.ref (Cmap.empty : struc_typ Cmap.t) ~name:"record-projs" -(* TODO: could be unify struc_typ and struc_tuple ? in particular, - is the inductive always (fst constructor) ? It seems so... *) +(* TODO: could be unify struc_typ and struc_tuple ? *) type struc_tuple = - inductive * constructor * (Name.t * bool) list * Constant.t option list + constructor * (Name.t * bool) list * Constant.t option list -let load_structure i (_,(ind,id,kl,projs)) = +let load_structure i (_, (id,kl,projs)) = let open Declarations in + let ind = fst id in let mib, mip = Global.lookup_inductive ind in let n = mib.mind_nparams in let struc = @@ -65,8 +65,7 @@ let load_structure i (_,(ind,id,kl,projs)) = let cache_structure o = load_structure 1 o -let subst_structure (subst,((kn,i),id,kl,projs as obj)) = - let kn' = subst_mind subst kn in +let subst_structure (subst, (id, kl, projs as obj)) = let projs' = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) @@ -75,10 +74,10 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) = projs in let id' = subst_constructor subst id in - if projs' == projs && kn' == kn && id' == id then obj else - ((kn',i),id',kl,projs') + if projs' == projs && id' == id then obj else + (id',kl,projs') -let discharge_structure (_,x) = Some x +let discharge_structure (_, x) = Some x let inStruc : struc_tuple -> obj = declare_object {(default_object "STRUCTURE") with @@ -88,8 +87,8 @@ let inStruc : struc_tuple -> obj = classify_function = (fun x -> Substitute x); discharge_function = discharge_structure } -let declare_structure (s,c,kl,pl) = - Lib.add_anonymous_leaf (inStruc (s,c,kl,pl)) +let declare_structure o = + Lib.add_anonymous_leaf (inStruc o) let lookup_structure indsp = Indmap.find indsp !structure_table diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 3e43372b65..53eb3fddf5 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -24,7 +24,7 @@ type struc_typ = { s_PROJ : Constant.t option list } type struc_tuple = - inductive * constructor * (Name.t * bool) list * Constant.t option list + constructor * (Name.t * bool) list * Constant.t option list val declare_structure : struc_tuple -> unit diff --git a/vernac/record.ml b/vernac/record.ml index 23274040b0..cb67548667 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -443,7 +443,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in let build = ConstructRef cstr in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in - let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in + let () = Recordops.declare_structure(cstr, List.rev kinds, List.rev sp_projs) in rsp in List.mapi map record_data |