diff options
| author | ppedrot | 2012-12-18 17:09:31 +0000 |
|---|---|---|
| committer | ppedrot | 2012-12-18 17:09:31 +0000 |
| commit | aa37087b8e7151ea96321a11012c1064210ef4ea (patch) | |
| tree | fff9ed837668746545832e3bd9f0a6dd99936ee4 /kernel/modops.ml | |
| parent | f61e682857596f0274b956295efd2bfba63bc8c0 (diff) | |
Modulification of Label
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index b81627f22b..e7afec2a05 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -44,24 +44,24 @@ type signature_mismatch_error = | NoTypeConstraintExpected type module_typing_error = - | SignatureMismatch of label * structure_field_body * signature_mismatch_error - | LabelAlreadyDeclared of label + | SignatureMismatch of Label.t * structure_field_body * signature_mismatch_error + | LabelAlreadyDeclared of Label.t | ApplicationToNotPath of module_struct_entry | NotAFunctor of struct_expr_body | IncompatibleModuleTypes of module_type_body * module_type_body | NotEqualModulePaths of module_path * module_path - | NoSuchLabel of label - | IncompatibleLabels of label * label + | NoSuchLabel of Label.t + | IncompatibleLabels of Label.t * Label.t | SignatureExpected of struct_expr_body | NoModuleToEnd | NoModuleTypeToEnd | NotAModule of string | NotAModuleType of string - | NotAConstant of label - | IncorrectWithConstraint of label - | GenerativeModuleExpected of label - | NonEmptyLocalContect of label option - | LabelMissing of label * string + | NotAConstant of Label.t + | IncorrectWithConstraint of Label.t + | GenerativeModuleExpected of Label.t + | NonEmptyLocalContect of Label.t option + | LabelMissing of Label.t * string exception ModuleTypingError of module_typing_error |