diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term_typing.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a566028d40..74c2e7da37 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -424,7 +424,10 @@ let export_side_effects mb env ce = let trusted = check_signatures mb signatures in let push_seff env = function | kn, cb, `Nothing, _ -> - Environ.add_constant kn cb env + let env = Environ.add_constant kn cb env in + if not cb.const_polymorphic then + Environ.push_context ~strict:true cb.const_universes env + else env | kn, cb, `Opaque(_, ctx), _ -> let env = Environ.add_constant kn cb env in Environ.push_context_set |