Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2005-03-27 20:14:28 -0800 (Sun, 27 Mar 2005)
Revision: 7059
Log message:

      Case analysis typing rule and reductions are ready.
      We don't have generic versions of them, instead instances are generated
      for each inductive type.
      For now, we don't write them anywhere - they are just printed (as terms).
      

Changes	Path
+218 -36	metaprl/theories/cic/cic_ind_cases.ml
+4 -2	metaprl/theories/cic/cic_ind_cases.mli
+4 -3	metaprl/theories/cic/cic_list.ml