diff options
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 8 |
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; |