diff options
Diffstat (limited to 'kernel/primred.mli')
| -rw-r--r-- | kernel/primred.mli | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/kernel/primred.mli b/kernel/primred.mli index 5531c81550..bbe564d8e7 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -12,6 +12,10 @@ val get_carry_constructors : env -> constructor * constructor val get_pair_constructor : env -> constructor val get_cmp_constructors : env -> constructor * constructor * constructor val get_f_cmp_constructors : env -> constructor * constructor * constructor * constructor +val get_f_class_constructors : + env -> constructor * constructor * constructor * constructor + * constructor * constructor * constructor * constructor + * constructor exception NativeDestKO (* Should be raised by get_* functions on failure *) @@ -37,6 +41,15 @@ module type RedNativeEntries = val mkFEq : env -> elem val mkFGt : env -> elem val mkFNotComparable : env -> elem + val mkPNormal : env -> elem + val mkNNormal : env -> elem + val mkPSubn : env -> elem + val mkNSubn : env -> elem + val mkPZero : env -> elem + val mkNZero : env -> elem + val mkPInf : env -> elem + val mkNInf : env -> elem + val mkNaN : env -> elem end module type RedNative = |