diff options
| author | Gaëtan Gilbert | 2020-11-11 21:11:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-13 12:53:00 +0100 |
| commit | e733f11f54cb847271c13f79538e8823c4d93038 (patch) | |
| tree | 4c790c0e0673d2afb2589b6eb0bed16105c21455 /kernel/cClosure.ml | |
| parent | 51e759fb2ff92dd89ab4823ddea3ea81be7f8046 (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.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; |
