Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-05-06 21:57:23 -0700 (Fri, 06 May 2005)
Revision: 7254
Log message:

      Typing of induction elimination operation (primitive recursion) is complete
      Conversions are to come.
      

Changes	Path
+1 -2	metaprl/theories/cic/cic_ind_elim_dep.ml
+26 -0	metaprl/theories/cic/cic_ind_elim_dep.mli
+355 -141	metaprl/theories/cic/cic_list.prla