eval_binary_double  447 eval.c         	eval_binary_double(inter, operator,
eval_binary_double  452 eval.c         	eval_binary_double(inter, operator,
eval_binary_double  458 eval.c         	eval_binary_double(inter, operator,