diff options
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index cab3276c39..7a9b12c430 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -72,7 +72,7 @@ let rec check_with_def env struc (idl,c) mp equiv = (* In the spirit of subtyping.check_constant, we accept any implementations of parameters and opaques terms, as long as they have the right type *) - let ccst = Declareops.constraints_of_constant cb in + let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in let env' = Environ.add_constraints ccst env' in let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> |