diff options
author | 2016-01-04 16:55:44 +0100 | |
---|---|---|
committer | 2016-01-04 16:56:54 +0100 | |
commit | bb9acba7cfe83ba3a5116b0e7aa78ac7f1219f60 (patch) | |
tree | 8be70fefaaa6f8130d098319b1463c28cfeb52fc | |
parent | d2b468a87cc50b1558feffc6cd3e1b866205c684 (diff) |
Fix handling of side-effects in case of `Opaque side-effects as well.
-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 |