diff options
| author | coqbot-app[bot] | 2021-03-26 14:17:20 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-26 14:17:20 +0000 |
| commit | c2ed2e395f2164ebbc550e70899c49af23e1ad1e (patch) | |
| tree | 62c140cd7785e416ccea19caf8a0cc05d2871cfb /kernel/vmvalues.ml | |
| parent | 71453f1643b55679d44caee30ce5541b5aa47263 (diff) | |
| parent | 5300e23cf5ac31fb835c5cfbe7ce1ed56f338f99 (diff) | |
Merge PR #14007: Never store persistent arrays as VM structured values.
Reviewed-by: silene
Diffstat (limited to 'kernel/vmvalues.ml')
| -rw-r--r-- | kernel/vmvalues.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 9944458d6b..938d1f28f7 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -459,8 +459,6 @@ let val_of_int i = (Obj.magic i : values) let val_of_uint i = (Obj.magic i : structured_values) -let val_of_parray p = (Obj.magic p : structured_values) - let atom_of_proj kn v = let r = Obj.new_block proj_tag 2 in Obj.set_field r 0 (Obj.repr kn); |