From e733f11f54cb847271c13f79538e8823c4d93038 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 11 Nov 2020 21:11:31 +0100
Subject: Remove unused CClosure.FNativeEntries.farray

BTW it was incorrect (array needs an instance)
---
 kernel/cClosure.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'kernel/cClosure.ml')

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;
-- 
cgit v1.2.3