diff options
| -rw-r--r-- | kernel/term_typing.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 74c2e7da3..aa60432a7 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -429,9 +429,11 @@ let export_side_effects mb env ce = 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 - ~strict:(not cb.const_polymorphic) ctx env in + let env = Environ.add_constant kn cb env in + if not cb.const_polymorphic then + let env = Environ.push_context ~strict:true cb.const_universes env in + Environ.push_context_set ~strict:true ctx env + else env in let rec translate_seff sl seff acc env = match sl, seff with | _, [] -> List.rev acc, ce |