Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-04-09 11:29:07 -0700 (Sat, 09 Apr 2005)
Revision: 7186
Log message:

      I think, I fixed the Dep rule by switching from generic ForAll1T1DT to a
      more custom ForAll1TConstr (which I also had to define).
      No it's time to try and see if it works the way it is intended to.
      

Changes  Path
+20 -4 metaprl/theories/cic/cic_ind_elim_dep.ml
+138 -1 metaprl/theories/cic/cic_ind_elim_dep.mli