aboutsummaryrefslogtreecommitdiff
path: root/kernel/cClosure.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-11-11 21:11:31 +0100
committerGaëtan Gilbert2020-11-13 12:53:00 +0100
commite733f11f54cb847271c13f79538e8823c4d93038 (patch)
tree4c790c0e0673d2afb2589b6eb0bed16105c21455 /kernel/cClosure.ml
parent51e759fb2ff92dd89ab4823ddea3ea81be7f8046 (diff)
Remove unused CClosure.FNativeEntries.farray
BTW it was incorrect (array needs an instance)
Diffstat (limited to 'kernel/cClosure.ml')
-rw-r--r--kernel/cClosure.ml8
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;