Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-22 14:41:17 -0800 (Sat, 22 Jan 2005)
Revision: 6472
Log message:

      - Added initial sequent type checking.
      - Upgraded CIC to single-conclusion sequents.
        For compatibility, added sequent args in the form
           sequent [|term|] { ... }
        where term is wrapped as << sequent_arg{term} >>.
      

Changes  Path
+1 -0 metaprl-branches/opname_classes2/filter/filter/filter_parse.ml
+19 -0 metaprl-branches/opname_classes2/filter/filter/term_grammar.ml
+59 -6 metaprl-branches/opname_classes2/refiner/reflib/term_ty_infer.ml
+16 -16 metaprl-branches/opname_classes2/refiner/term_ds/term_man_ds.ml
+2 -0 metaprl-branches/opname_classes2/support/display/perv.ml
+2 -0 metaprl-branches/opname_classes2/support/display/perv.mli
+9 -9 metaprl-branches/opname_classes2/support/tactics/dtactic.ml
+8 -7 metaprl-branches/opname_classes2/support/tactics/top_conversionals.ml
+16 -12 metaprl-branches/opname_classes2/support/tactics/top_tacticals.ml
+0 -0 metaprl-branches/opname_classes2/support/tactics/top_tacticals.mli
+2 -1 metaprl-branches/opname_classes2/theories/base/base_reflection.ml
+2 -1 metaprl-branches/opname_classes2/theories/base/base_reflection.mli
+1 -1 metaprl-branches/opname_classes2/theories/base/base_rewrite.ml
+1 -1 metaprl-branches/opname_classes2/theories/base/base_rewrite.mli
+98 -103 metaprl-branches/opname_classes2/theories/cic/cic_ind_cases.ml
+291 -295 metaprl-branches/opname_classes2/theories/cic/cic_ind_type.ml
+85 -85 metaprl-branches/opname_classes2/theories/cic/cic_ind_type.mli
+7 -2 metaprl-branches/opname_classes2/theories/cic/cic_lambda.ml
+4 -1 metaprl-branches/opname_classes2/theories/cic/cic_lambda.mli
+18 -18 metaprl-branches/opname_classes2/theories/cic/cic_list.ml
+1 -1 metaprl-branches/opname_classes2/theories/experimental/compile/m_ir.ml
+1 -1 metaprl-branches/opname_classes2/theories/experimental/compile/m_ir.mli
+9 -9 metaprl-branches/opname_classes2/theories/itt/itt_record_renaming.ml