diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 3a75004b0..12699b02b 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -13,7 +13,6 @@ open Names open Globnames open Nameops open Term -open Context open Vars open Environ open Declarations @@ -148,8 +147,8 @@ let typecheck_params_and_fields def id pl t ps nots fs = else arity, evars in let evars, nf = Evarutil.nf_evars_and_universes evars in - let newps = map_rel_context nf newps in - let newfs = map_rel_context nf newfs in + let newps = Context.Rel.map nf newps in + let newfs = Context.Rel.map nf newfs in let ce t = Evarutil.check_evars env0 Evd.empty evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps); List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs); @@ -244,8 +243,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let ctx = Univ.instantiate_univ_context mib.mind_universes in let indu = indsp, u in let r = mkIndU (indsp,u) in - let rp = applist (r, Context.extended_rel_list 0 paramdecls) in - let paramargs = Context.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) + let rp = applist (r, Context.Rel.to_extended_list 0 paramdecls) in + let paramargs = Context.Rel.to_extended_list 1 paramdecls in (*def in [[params;x:rp]]*) let x = Name binder_name in let fields = instantiate_possibly_recursive_type indu paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in @@ -353,7 +352,7 @@ open Typeclasses let declare_structure finite poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in - let args = Context.extended_rel_list nfields params in + let args = Context.Rel.to_extended_list nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in let binder_name = |