Merge PR #13356: Make the universe of primitive arrays irrelevant

Reviewed-by: ppedrot

1 files changed, 1 insertions, 7 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 174125fc57..17feeb9b5a 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -1098,14 +1098,8 @@ module FNativeEntries =
 
     let defined_array = ref false
 
-    let farray = ref dummy
-
     let init_array retro =
-      match retro.Retroknowledge.retro_array with
-      | Some c ->
-        defined_array := true;
-        farray := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
-      | None -> defined_array := false
+      defined_array := Option.has_some retro.Retroknowledge.retro_array
 
     let init env =
       current_retro := env.retroknowledge;