Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-03 15:51:57 -0800 (Tue, 03 Feb 2004)
Revision: 5339
Log message:

      - For prim rules, check whether the specified extract is "universal".
      - Fixed a number of places where a non-universal extract was specified.
      

Changes	Path
+75 -21	metaprl/refiner/refiner/refine.ml
+4 -0	metaprl/refiner/reflib/refine_exn.ml
+14 -35	metaprl/theories/itt/itt_disect.ml
+3 -3	metaprl/theories/itt/itt_prec.ml
+2 -2	metaprl/theories/itt/itt_quotient.ml
+2 -2	metaprl/theories/itt/itt_rfun.ml
+4 -4	metaprl/theories/itt/itt_squiggle.ml
+11 -6	metaprl/theories/itt/itt_subtype.ml
+2515 -2415	metaprl/theories/itt/itt_subtype.prla