Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-07 00:45:04 -0700 (Mon, 07 Apr 2003)
Revision: 4392
Log message:

      - Using the new syntax, got rid of some unused binding vars
      - The rule itt_rfun.well_founded_assum_elim had a wrong "squash" marker.
      

Changes  Path
+3 -1 metaprl/filter/base/term_grammar.ml
+1 -1 metaprl/theories/itt/itt_equal.ml
+1 -1 metaprl/theories/itt/itt_equal.mli
+2 -2 metaprl/theories/itt/itt_esquash.ml
+2 -2 metaprl/theories/itt/itt_quotient.ml
+4 -4 metaprl/theories/itt/itt_quotient.mli
+2 -2 metaprl/theories/itt/itt_rfun.ml
+1 -1 metaprl/theories/itt/itt_rfun.mli
+2 -2 metaprl/theories/itt/itt_set.ml
+2 -2 metaprl/theories/itt/itt_set.mli
+14 -14 metaprl/theories/itt/itt_squash.ml
+5 -5 metaprl/theories/itt/itt_squash.mli
+1 -1 metaprl/theories/itt/itt_squiggle.ml
+2 -2 metaprl/theories/itt/itt_struct.ml
+2 -2 metaprl/theories/itt/itt_struct.mli
+3 -3 metaprl/theories/itt/itt_subtype.ml
+2 -2 metaprl/theories/itt/itt_subtype.mli
+4 -4 metaprl/theories/itt/itt_union.ml
+4 -4 metaprl/theories/itt/itt_union.mli
+1 -1 metaprl/theories/itt/itt_unit.ml
+1 -1 metaprl/theories/itt/itt_unit.mli