Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-21 22:28:18 -0700 (Wed, 21 Apr 2004)
Revision: 5692
Log message:

      [Bug 129] Got rid of the eqcd resource and the eqcdT tactic.
      

Changes  Path
+2 -2 metaprl/theories/itt/itt_atom.ml
+2 -2 metaprl/theories/itt/itt_bisect.ml
+6 -6 metaprl/theories/itt/itt_bool.ml
+10 -23 metaprl/theories/itt/itt_bunion.ml
+2 -2 metaprl/theories/itt/itt_dfun.ml
+2 -2 metaprl/theories/itt/itt_disect.ml
+4 -4 metaprl/theories/itt/itt_dprod.ml
+3 -3 metaprl/theories/itt/itt_dprod_imp.ml
+5 -90 metaprl/theories/itt/itt_equal.ml
+0 -7 metaprl/theories/itt/itt_equal.mli
+1 -1 metaprl/theories/itt/itt_esquash.ml
+7 -7 metaprl/theories/itt/itt_fun.ml
+2 -2 metaprl/theories/itt/itt_group.ml
+8 -8 metaprl/theories/itt/itt_int_base.ml
+7 -7 metaprl/theories/itt/itt_int_ext.ml
+3 -3 metaprl/theories/itt/itt_isect.ml
+2 -2 metaprl/theories/itt/itt_list.ml
+9 -9 metaprl/theories/itt/itt_logic.ml
+1 -1 metaprl/theories/itt/itt_nat.ml
+1 -1 metaprl/theories/itt/itt_nequal.ml
+1 -1 metaprl/theories/itt/itt_poly.ml
+1 -1 metaprl/theories/itt/itt_poly.prla
+3 -3 metaprl/theories/itt/itt_prec.ml
+2 -2 metaprl/theories/itt/itt_prod.ml
+1 -1 metaprl/theories/itt/itt_quotient.ml
+1 -1 metaprl/theories/itt/itt_record_label.ml
+3 -3 metaprl/theories/itt/itt_rfun.ml
+2 -2 metaprl/theories/itt/itt_set.ml
+1 -1 metaprl/theories/itt/itt_singleton.ml
+2 -2 metaprl/theories/itt/itt_squash.ml
+2 -2 metaprl/theories/itt/itt_squiggle.ml
+2 -2 metaprl/theories/itt/itt_srec.ml
+3 -3 metaprl/theories/itt/itt_subset.ml
+2 -2 metaprl/theories/itt/itt_subtype.ml
+9 -25 metaprl/theories/itt/itt_tunion.ml
+4 -4 metaprl/theories/itt/itt_union.ml
+2 -2 metaprl/theories/itt/itt_unit.ml
+1 -1 metaprl/theories/itt/itt_void.ml
+3 -3 metaprl/theories/itt/itt_w.ml