Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2007-08-31 09:38:15 -0700 (Fri, 31 Aug 2007)
Revision: 12063
Log message:

      1.Coq uses same rules for statements of the form 'T' and 't in T', we had to add some extra rules to support it, which finally brought extracts into the theory.
     2.Added some thinning rules
     3.Added cut rule, we could not find it among Coq rules but there is a tactic which does what assertT does in ITT, so cut has to be in CIC at least in some form
     4.level parameters' arithmetic was not properly done, fixed
     5.added some annotation but we actually need to write a tactic to deduce term types 
     6.Started to work on conjunction, which is defined as a recursive type in CIC

Changes  Path(relative to metaprl/theories/cic)
+2 -0 MetaprlInfo
+5 -1 cic_ind_elim_dep.ml
+7 -2 cic_ind_type.ml
+2 -1 cic_ind_type.mli
+89 -26 cic_lambda.ml
+36 -4 cic_lambda.mli
Added cic_prop_connectives.ml
Properties cic_prop_connectives.ml
Added cic_prop_connectives.mli
Properties cic_prop_connectives.mli
Added cic_prop_connectives.prla
Properties cic_prop_connectives.prla
Added minimal_logic.ml
Properties minimal_logic.ml
Added minimal_logic.mli
Properties minimal_logic.mli
Added minimal_logic.prla
Properties minimal_logic.prla