Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-25 20:42:20 -0700 (Wed, 25 Jul 2001)
Revision: 3348
Log message:

      I changed the rule subtypeElimination2 and proved use_subtype1.
      Now elimination rule for subtyping request one or two term parameters.
      With one parameter it works as usual, with two params 'a and 'b it produces
      a subgoal 'a='b in 'A.
      

Changes	Path
+14 -14	metaprl/theories/itt/itt_subtype.ml
+3 -3	metaprl/theories/itt/itt_subtype.mli
+2332 -2092	metaprl/theories/itt/itt_subtype.prla