diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 084628a4e..51b4ca39c 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -29,8 +29,8 @@ type signature_mismatch_error = | DefinitionFieldExpected | ModuleFieldExpected | ModuleTypeFieldExpected - | NotConvertibleInductiveField of identifier - | NotConvertibleConstructorField of identifier + | NotConvertibleInductiveField of Id.t + | NotConvertibleConstructorField of Id.t | NotConvertibleBodyField | NotConvertibleTypeField | NotSameConstructorNamesField |