diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-30 10:05:14 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-05 12:51:49 +0100 |
| commit | 76579aff8f8534cbc990b5ea2652b33655512213 (patch) | |
| tree | 9a4af0643f42d2643b487412f644a0ad3a14e47a /kernel/nativevalues.mli | |
| parent | 55b2a4e0c24d691b71256c91ed54e245efce340b (diff) | |
[native_compute] Remove useless conversion to list in reification.
Diffstat (limited to 'kernel/nativevalues.mli')
| -rw-r--r-- | kernel/nativevalues.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 18b877745..17d6978cd 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -84,7 +84,7 @@ val napply : t -> t array -> t val dummy_value : unit -> t val atom_of_accu : accumulator -> atom -val args_of_accu : accumulator -> t list +val args_of_accu : accumulator -> t array val accu_nargs : accumulator -> int val cast_accu : t -> accumulator |