diff options
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 11 | ||||
| -rw-r--r-- | kernel/byterun/coq_values.h | 6 |
2 files changed, 8 insertions, 9 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 55b973dcdb..74edd79872 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1551,19 +1551,16 @@ value coq_interprete x = Double_val(accu); y = Double_val(*sp++); if(x < y) { - Alloc_small(accu, 1, coq_tag_Some); - Field(accu, 0) = coq_Lt; + accu = coq_FLt; } else if(x > y) { - Alloc_small(accu, 1, coq_tag_Some); - Field(accu, 0) = coq_Gt; + accu = coq_FGt; } else if(x == y) { - Alloc_small(accu, 1, coq_tag_Some); - Field(accu, 0) = coq_Eq; + accu = coq_FEq; } else { // nan value - accu = coq_None; + accu = coq_FNotComparable; } Next; } diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index fa51b2d31f..c79a8f1b4f 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -42,8 +42,10 @@ #define coq_Eq Val_int(0) #define coq_Lt Val_int(1) #define coq_Gt Val_int(2) -#define coq_tag_Some 1 -#define coq_None Val_int(0) +#define coq_FEq Val_int(0) +#define coq_FLt Val_int(1) +#define coq_FGt Val_int(2) +#define coq_FNotComparable Val_int(3) #define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */ |