diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 76915e917a..11e6be6598 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -17,7 +17,7 @@ open Util open Names -open Term +open Constr open Declarations open Declareops open Environ @@ -59,7 +59,7 @@ type module_typing_error = | NotAFunctor | IsAFunctor | IncompatibleModuleTypes of module_type_body * module_type_body - | NotEqualModulePaths of module_path * module_path + | NotEqualModulePaths of ModPath.t * ModPath.t | NoSuchLabel of Label.t | IncompatibleLabels of Label.t * Label.t | NotAModule of string @@ -68,7 +68,7 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string - | IncludeRestrictedFunctor of module_path + | IncludeRestrictedFunctor of ModPath.t exception ModuleTypingError of module_typing_error @@ -266,9 +266,9 @@ let subst_structure subst = subst_structure subst do_delta_codom (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) let add_retroknowledge mp = let perform rkaction env = match rkaction with - |Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> + | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> Environ.register env f e - |_ -> + | _ -> CErrors.anomaly ~label:"Modops.add_retroknowledge" (Pp.str "had to import an unsupported kind of term.") in @@ -403,8 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta = let constr = Mod_subst.force_constr body in add_inline_delta_resolver kn (lev, Some constr) l with Not_found -> - error_no_such_label_sub (con_label con) - (string_of_mp (con_modpath con)) + error_no_such_label_sub (Constant.label con) + (ModPath.to_string (Constant.modpath con)) in make_inline delta constants |