Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-03-27 20:25:22 -0800 (Sun, 27 Mar 2005)
Revision: 7060
Log message:

      Doing fixpoint rules via instances seems impossible;
      Generic fixpoint typing rule is way to complex (and reportedly
      the main source of bugs in Coq).
      So we stopped doing case+fixpoint instead we started to implement
      ITT-style induction operations (like list_ind) - in CIC they
      are called elimination rules.
      Coq community do not like them because they are not as natural to use
      as case+fixpoint but they are present in Coq.
      

Changes	Path
Properties	metaprl/theories/cic
+2 -1	metaprl/theories/cic/OMakefile
Added	metaprl/theories/cic/cic_ind_elim.ml
Properties	metaprl/theories/cic/cic_ind_elim.ml
Added	metaprl/theories/cic/cic_ind_elim.mli
Properties	metaprl/theories/cic/cic_ind_elim.mli
+0 -2	metaprl/theories/cic/cic_list.ml