Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-10 22:31:14 -0700 (Thu, 10 Jun 1999)
Revision: 2702
Log message:

      Fixed level_lt and level_le.  Now the universeEquality rule no longer
      proves << member{univ[i:l]; univ[i:l]} >>, and it does prove
      << member{univ[i|j ':l]; univ[j:l]} >> (it got both of these cases
      wrong before).
      

Changes	Path
+8 -8	metaprl/refiner/term_ds/term_man_ds.ml
+8 -8	metaprl/refiner/term_gen/term_man_gen.ml