diff options
Diffstat (limited to 'kernel/byterun/coq_fix_code.c')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 0865487c98..bca2cc3bd9 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -63,7 +63,12 @@ void init_arity () { arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]= arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]= arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= - arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=1; + arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]= + arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]= + arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= + arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= + arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= + arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[PROJ]=2; |