... provided in this patch.<br><br>I have a couple of questions. One is whether NULL-POINTER has to cons a new pointer _every_time_. It would be more clever to create a variable and put the pointer there.<br><br>The other one is whether MAKE-POINTER is used at all, given that we have pointer increment / decrement operations.<br>

<br>Juanjo<br clear="all"><br>-- <br>Instituto de Física Fundamental, CSIC<br>c/ Serrano, 113b, Madrid 28006 (Spain) <br><a href="http://tream.dreamhosters.com">http://tream.dreamhosters.com</a><br>