diff options
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 |