diff options
| -rw-r--r-- | kernel/vmlambda.ml | 4 | ||||
| -rw-r--r-- | kernel/vmvalues.ml | 2 | ||||
| -rw-r--r-- | kernel/vmvalues.mli | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_14006.v | 3 |
4 files changed, 3 insertions, 7 deletions
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml index e353348ac7..ee32384ec9 100644 --- a/kernel/vmlambda.ml +++ b/kernel/vmlambda.ml @@ -494,10 +494,6 @@ let makeblock tag nparams arity args = else Lmakeblock(tag, args) let makearray args def = - try - let p = Array.map get_value args in - Lval (val_of_parray @@ Parray.unsafe_of_array p (get_value def)) - with Not_found -> let ar = Lmakeblock(0, args) in (* build the ocaml array *) let kind = Lmakeblock(0, [|ar; def|]) in (* Parray.Array *) Lmakeblock(0,[|kind|]) (* the reference *) 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); diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index d15595766a..534a85d773 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -148,7 +148,6 @@ val val_of_atom : atom -> values val val_of_int : int -> structured_values val val_of_block : tag -> structured_values array -> structured_values val val_of_uint : Uint63.t -> structured_values -val val_of_parray : structured_values Parray.t -> structured_values external val_of_annot_switch : annot_switch -> values = "%identity" external val_of_proj_name : Projection.Repr.t -> values = "%identity" diff --git a/test-suite/bugs/closed/bug_14006.v b/test-suite/bugs/closed/bug_14006.v new file mode 100644 index 0000000000..b857959ae9 --- /dev/null +++ b/test-suite/bugs/closed/bug_14006.v @@ -0,0 +1,3 @@ +From Coq Require Import Int63 PArray. +Definition t : array nat := [| 1; 3; 2 | 4 |]. +Definition vm_accu_set v := Eval vm_compute in t.[1 <- v]. |