diff options
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index d3cd6b62a5..4941d64d82 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1863,8 +1863,9 @@ let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with | None -> let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes - else Univ.Instance.empty + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.AUContext.instance ctx in begin match cb.const_body with | Def t -> @@ -1960,7 +1961,7 @@ let param_name = Name (id_of_string "params") let arg_name = Name (id_of_string "arg") let compile_mind prefix ~interactive mb mind stack = - let u = Declareops.inductive_instance mb in + let u = Declareops.inductive_polymorphic_instance mb in let f i stack ob = let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in let j = push_symbol (SymbInd (mind,i)) in |