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 |