diff options
Diffstat (limited to 'kernel/primred.mli')
| -rw-r--r-- | kernel/primred.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/primred.mli b/kernel/primred.mli index bbe564d8e7..1bfaffaa44 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -24,10 +24,12 @@ module type RedNativeEntries = type elem type args type evd (* will be unit in kernel, evar_map outside *) + type uinstance val get : args -> int -> elem val get_int : evd -> elem -> Uint63.t val get_float : evd -> elem -> Float64.t + val get_parray : evd -> elem -> elem Parray.t val mkInt : env -> Uint63.t -> elem val mkFloat : env -> Float64.t -> elem val mkBool : env -> bool -> elem @@ -50,6 +52,7 @@ module type RedNativeEntries = val mkPInf : env -> elem val mkNInf : env -> elem val mkNaN : env -> elem + val mkArray : env -> uinstance -> elem Parray.t -> elem -> elem end module type RedNative = @@ -57,7 +60,8 @@ module type RedNative = type elem type args type evd - val red_prim : env -> evd -> CPrimitives.t -> args -> elem option + type uinstance + val red_prim : env -> evd -> CPrimitives.t -> uinstance -> args -> elem option end module RedNative : @@ -65,3 +69,4 @@ module RedNative : RedNative with type elem = E.elem with type args = E.args with type evd = E.evd + with type uinstance = E.uinstance |