Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-05 23:26:04 -0700 (Sat, 05 Jun 1999)
Revision: 2691
Log message:

      Added a new primitive rule universeCumulativity and corresponding
      tactic cumulativityT.
      

Changes  Path
+4 -0 metaprl/doc/itt_quickref.txt
+19 -0 metaprl/theories/itt/itt_equal.ml
+1 -0 metaprl/theories/itt/itt_equal.mli