Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-22 23:22:12 -0700 (Sun, 22 May 2005)
Revision: 7317
Log message:
Added the enforcement of non-recursivity of definitions (i.e. of the fact that
the shape being define can not occur on the RHS of the definition) to the
refiner.
Note: this used to be enforced by the filter, but now that filter allows
omiting from .ml declarations that are already present in .mli,
non-recursivity is no longer enforced by the filter. And in any case, this is
a correctness issue, so it should be enforced by the refiner.