Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-12-30 10:47:38 -0800 (Thu, 30 Dec 2004)
Revision: 6369
Log message:

      We are exploring another approach - instead of giving universal rules for cases
      analysis and fixpoint we want to generate specific instances of these rules for
      individual inductive types automatically.
      

Changes  Path
+172 -43 metaprl/theories/cic/cic_ind_cases.ml
+4 -0 metaprl/theories/cic/cic_ind_cases.mli
+4 -0 metaprl/theories/cic/cic_ind_type.ml
+12 -0 metaprl/theories/cic/cic_ind_type.mli
+10 -0 metaprl/theories/cic/cic_lambda.ml
+8 -0 metaprl/theories/cic/cic_lambda.mli
+20 -0 metaprl/theories/cic/cic_list.ml