Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 19:51:33 -0800 (Thu, 03 Feb 2005)
Revision: 6590
Log message:

      - Removed the obsolte "Opname" and "Definition" choices from the summary_item
        type (Filter_summary has hack that prevents it from complaining about
        unknown "opname" and "definition" items in the old .prla)
      
      - Restored the ability to have a declare+rewrite in the interface and a define
        in the implementation.
      
      - Made the ls options processor a bit smarter about the new "declare" items.
        In particular, an ordinary "declare" directive is going to be consideted
        formal when the type does not mention "Dform" and is going to be considered
        informal and display-related when it does.
      

Changes  Path
+3 -31 metaprl-branches/opname_classes4/filter/base/filter_cache_fun.ml
+7 -4 metaprl-branches/opname_classes4/filter/base/filter_magic.ml
+18 -122 metaprl-branches/opname_classes4/filter/base/filter_summary.ml
+0 -13 metaprl-branches/opname_classes4/filter/base/filter_type.ml
+0 -2 metaprl-branches/opname_classes4/filter/filter/filter_parse.ml
+0 -18 metaprl-branches/opname_classes4/filter/filter/filter_prog.ml
+7 -0 metaprl-branches/opname_classes4/support/display/perv.ml
+3 -0 metaprl-branches/opname_classes4/support/display/perv.mli
+34 -46 metaprl-branches/opname_classes4/support/display/summary.ml
+2 -4 metaprl-branches/opname_classes4/support/shell/shell_core.ml
+6 -6 metaprl-branches/opname_classes4/support/shell/shell_package.ml
+10 -7 metaprl-branches/opname_classes4/support/shell/shell_rule.ml
+3 -1 metaprl-branches/opname_classes4/support/shell/shell_rule.mli
+5 -5 metaprl-branches/opname_classes4/theories/itt/itt_logic.ml