Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-04-27 19:22:22 -0700 (Wed, 27 Apr 2005)
Revision: 7232
Log message:

      Some fixes and improvements in cic_ind_elim*
      Removed bind-parameters where they are not needed anymore,
      added intro-annotation in several places
      

Changes	Path
+2 -2	metaprl/theories/cic/OMakefile
+24 -5	metaprl/theories/cic/cic_ind_elim.ml
+1 -0	metaprl/theories/cic/cic_ind_elim.mli
+17 -4	metaprl/theories/cic/cic_ind_elim_dep.ml
+2 -1	metaprl/theories/cic/cic_ind_elim_dep.mli
+9 -9	metaprl/theories/cic/cic_ind_type.ml
+6 -6	metaprl/theories/cic/cic_ind_type.mli
+20 -23	metaprl/theories/cic/cic_lambda.ml
+32 -32	metaprl/theories/cic/cic_lambda.mli
+12 -0	metaprl/theories/cic/cic_list.ml