diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 58 |
1 files changed, 29 insertions, 29 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index bbf160db21..f43dbd88f9 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -47,11 +47,9 @@ type signature_mismatch_error = | RecordFieldExpected of bool | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases - | NoTypeConstraintExpected - | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types - | IncompatibleConstraints of Univ.AUContext.t + | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t } type module_typing_error = | SignatureMismatch of @@ -130,16 +128,16 @@ let destr_nofunctor = function |NoFunctor a -> a |MoreFunctor _ -> error_is_a_functor () -let rec functor_smartmap fty f0 funct = match funct with +let rec functor_smart_map fty f0 funct = match funct with |MoreFunctor (mbid,ty,e) -> let ty' = fty ty in - let e' = functor_smartmap fty f0 e in + let e' = functor_smart_map fty f0 e in if ty==ty' && e==e' then funct else MoreFunctor (mbid,ty',e') |NoFunctor a -> let a' = f0 a in if a==a' then funct else NoFunctor a' let rec functor_iter fty f0 = function - |MoreFunctor (mbid,ty,e) -> fty ty; functor_iter fty f0 e + |MoreFunctor (_mbid,ty,e) -> fty ty; functor_iter fty f0 e |NoFunctor a -> f0 a (** {6 Misc operations } *) @@ -172,7 +170,7 @@ let implem_iter fs fa impl = match impl with (** {6 Substitutions of modular structures } *) -let id_delta x y = x +let id_delta x _y = x let subst_with_body sub = function |WithMod(id,mp) as orig -> @@ -197,11 +195,11 @@ let rec subst_structure sub do_delta sign = let mtb' = subst_modtype sub do_delta mtb in if mtb==mtb' then orig else (l,SFBmodtype mtb') in - List.smartmap subst_body sign + List.Smart.map subst_body sign and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = fun is_mod sub subst_impl do_delta mb -> - let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty } = mb in + let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty; _ } = mb in let mp' = subst_mp sub mp in let sub = if ModPath.equal mp mp' then sub @@ -210,7 +208,7 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> in let ty' = subst_signature sub do_delta ty in let me' = subst_impl sub me in - let aty' = Option.smartmap (subst_expression sub id_delta) aty in + let aty' = Option.Smart.map (subst_expression sub id_delta) aty in let delta' = do_delta mb.mod_delta sub in if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta then mb @@ -245,12 +243,12 @@ and subst_expr sub do_delta seb = match seb with if meb==meb' && wdb==wdb' then seb else MEwith(meb',wdb') and subst_expression sub do_delta = - functor_smartmap + functor_smart_map (subst_modtype sub do_delta) (subst_expr sub do_delta) and subst_signature sub do_delta = - functor_smartmap + functor_smart_map (subst_modtype sub do_delta) (subst_structure sub do_delta) @@ -266,9 +264,9 @@ let subst_structure subst = subst_structure subst do_delta_codom (* spiwack: here comes the function which takes care of importing the retroknowledge declared in the library *) (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) -let add_retroknowledge mp = +let add_retroknowledge = let perform rkaction env = match rkaction with - | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> + | Retroknowledge.RKRegister (f, ((GlobRef.ConstRef _ | GlobRef.IndRef _) as e)) -> Environ.register env f e | _ -> CErrors.anomaly ~label:"Modops.add_retroknowledge" @@ -290,10 +288,10 @@ let add_retroknowledge mp = let rec add_structure mp sign resolver linkinfo env = let add_one env (l,elem) = match elem with |SFBconst cb -> - let c = constant_of_delta_kn resolver (KerName.make2 mp l) in + let c = constant_of_delta_kn resolver (KerName.make mp l) in Environ.add_constant_key c cb linkinfo env |SFBmind mib -> - let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in + let mind = mind_of_delta_kn resolver (KerName.make mp l) in let mib = if mib.mind_private != None then { mib with mind_private = Some true } @@ -310,7 +308,7 @@ and add_module mb linkinfo env = let env = Environ.shallow_add_module mb env in match mb.mod_type with |NoFunctor struc -> - add_retroknowledge mp mb.mod_retroknowledge + add_retroknowledge mb.mod_retroknowledge (add_structure mp struc mb.mod_delta linkinfo env) |MoreFunctor _ -> env @@ -332,7 +330,7 @@ let strengthen_const mp_from l cb resolver = match cb.const_body with |Def _ -> cb |_ -> - let kn = KerName.make2 mp_from l in + let kn = KerName.make mp_from l in let con = constant_of_delta_kn resolver kn in let u = match cb.const_universes with @@ -340,7 +338,8 @@ let strengthen_const mp_from l cb resolver = | Polymorphic_const ctx -> Univ.make_abstract_instance ctx in { cb with - const_body = Def (Mod_subst.from_val (mkConstU (con,u))); + const_body = Def (Mod_subst.from_val (mkConstU (con,u))); + const_private_poly_univs = None; const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) } let rec strengthen_mod mp_from mp_to mb = @@ -372,7 +371,7 @@ and strengthen_sig mp_from struc mp_to reso = match struc with let item' = l,SFBmodule mb' in let reso',rest' = strengthen_sig mp_from rest mp_to reso in add_delta_resolver reso' mb.mod_delta, item':: rest' - |(l,SFBmodtype mty as item) :: rest -> + |(_l,SFBmodtype _mty as item) :: rest -> let reso',rest' = strengthen_sig mp_from rest mp_to reso in reso',item::rest' @@ -403,7 +402,8 @@ let inline_delta_resolver env inl mp mbid mtb delta = | Undef _ | OpaqueDef _ -> l | Def body -> let constr = Mod_subst.force_constr body in - add_inline_delta_resolver kn (lev, Some constr) l + let ctx = Declareops.constant_polymorphic_context constant in + add_inline_delta_resolver kn (lev, Some (ctx, constr)) l with Not_found -> error_no_such_label_sub (Constant.label con) (ModPath.to_string (Constant.modpath con)) @@ -450,8 +450,8 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso = (* If we are performing an inclusion we need to add the fact that the constant mp_to.l is \Delta-equivalent to reso(mp_from.l) *) - let kn_from = KerName.make2 mp_from l in - let kn_to = KerName.make2 mp_to l in + let kn_from = KerName.make mp_from l in + let kn_to = KerName.make mp_to l in let old_name = kn_of_delta reso kn_from in add_kn_delta_resolver kn_to old_name reso', str' else @@ -471,8 +471,8 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso = in (* Same as constant *) if incl then - let kn_from = KerName.make2 mp_from l in - let kn_to = KerName.make2 mp_to l in + let kn_from = KerName.make mp_from l in + let kn_to = KerName.make mp_to l in let old_name = kn_of_delta reso kn_from in add_kn_delta_resolver kn_to old_name reso', str' else @@ -595,13 +595,13 @@ and clean_field l field = match field with if mb==mb' then field else (lab,SFBmodule mb') |_ -> field -and clean_structure l = List.smartmap (clean_field l) +and clean_structure l = List.Smart.map (clean_field l) and clean_signature l = - functor_smartmap (clean_module_type l) (clean_structure l) + functor_smart_map (clean_module_type l) (clean_structure l) and clean_expression l = - functor_smartmap (clean_module_type l) (fun me -> me) + functor_smart_map (clean_module_type l) (fun me -> me) let rec collect_mbid l sign = match sign with |MoreFunctor (mbid,ty,m) -> @@ -628,7 +628,7 @@ let join_structure except otab s = let rec join_module : 'a. 'a generic_module_body -> unit = fun mb -> Option.iter join_expression mb.mod_type_alg; join_signature mb.mod_type - and join_field (l,body) = match body with + and join_field (_l,body) = match body with |SFBconst sb -> join_constant_body except otab sb |SFBmind _ -> () |SFBmodule m -> |