From 012f5fb722a9d5dcef82c800aa54ed50c0a58957 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 10 Jul 2017 19:11:20 +0200 Subject: Safe API for accessing universe constraints of global references. Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel. --- kernel/nativecode.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/nativecode.ml') diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 9d7262206..da7fcd6f2 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1959,14 +1959,14 @@ 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_polymorphic_instance mb in + let u = Declareops.inductive_polymorphic_context 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 let name = Gind ("", (mind, i)) in let accu = let args = - if Univ.Instance.is_empty u then + if Int.equal (Univ.AUContext.size u) 0 then [|get_ind_code j; MLarray [||]|] else [|get_ind_code j|] in -- cgit v1.2.3