diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a566028d..510f4354 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -424,11 +424,16 @@ 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 - ~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 |