From b6fadbf6f08860609961f6dbad8a036346925265 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 31 Aug 2020 14:50:59 +0200 Subject: Make callback opcodes more generic. This does not make the code any slower, since Is_coq_array(accu) && Is_uint63(sp[0]) and !Is_accu(accu) && !Is_accu(sp[0]) take the exact same number of tests to pass in the concrete case. In the accumulator case, it takes one more test to fail, but we do not care about the performances then. --- kernel/genOpcodeFiles.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/genOpcodeFiles.ml') diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index c8c8f61d59..63abb50cc2 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -147,10 +147,10 @@ let opcodes = "CHECKLDSHIFTEXP"; "CHECKNEXTUPFLOAT"; "CHECKNEXTDOWNFLOAT"; - "ISINT_CAML_CALL2"; - "ISARRAY_CAML_CALL1"; - "ISARRAY_INT_CAML_CALL2"; - "ISARRAY_INT_CAML_CALL3"; + "CHECKCAMLCALL2_1"; + "CHECKCAMLCALL1"; + "CHECKCAMLCALL2"; + "CHECKCAMLCALL3_1"; "STOP" |] -- cgit v1.2.3