diff options
| author | Gaëtan Gilbert | 2018-11-09 16:31:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-09 16:31:32 +0100 |
| commit | 1761f8ed41f3891f8b6edc0dd256cd18e47a74fb (patch) | |
| tree | 754bd11791e63df535dff44a58e126ff9330b8ea /kernel/term_typing.ml | |
| parent | 5d90e05b35f85607c43888b9adb0319e98a81fb4 (diff) | |
| parent | 8272c4e08f3c045a27d0bcb89a67a167625bf233 (diff) | |
Merge PR #8601: Move bound universe names to abstract contexts
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index fb1b3e236c..35fa871b4e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -68,8 +68,8 @@ let feedback_completion_typecheck = let abstract_constant_universes = function | Monomorphic_const_entry uctx -> Univ.empty_level_subst, Monomorphic_const uctx - | Polymorphic_const_entry uctx -> - let sbst, auctx = Univ.abstract_universes uctx in + | Polymorphic_const_entry (nas, uctx) -> + let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in sbst, Polymorphic_const auctx @@ -78,7 +78,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | ParameterEntry (ctx,(t,uctx),nl) -> let env = match uctx with | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env - | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env + | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env in let j = infer env t in let usubst, univs = abstract_constant_universes uctx in @@ -150,7 +150,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let ctx = Univ.ContextSet.union univs ctx in let env = push_context_set ~strict:true ctx env in env, Univ.empty_level_subst, Monomorphic_const ctx - | Polymorphic_const_entry uctx -> + | Polymorphic_const_entry (nas, uctx) -> (** Ensure not to generate internal constraints in polymorphic mode. The only way for this to happen would be that either the body contained deferred universes, or that it contains monomorphic @@ -160,7 +160,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = i.e. [trust] is always [Pure]. *) let () = assert (Univ.ContextSet.is_empty ctx) in let env = push_context ~strict:false uctx env in - let sbst, auctx = Univ.abstract_universes uctx in + let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in env, sbst, Polymorphic_const auctx in |