Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-03-24 20:25:28 -0800 (Wed, 24 Mar 2004)
Revision: 5550
Log message:

      First compilable version (with some workaround of bug175)
      It has inductive definitions without one very complicated case of
      positivity condition on terms.
      Case analysis and fixpoint is not implemented yet.
      And it's very ugly yet.
      

Changes	Path
+162 -153	metaprl/theories/cic/rules.ml