Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-19 17:27:36 -0700 (Tue, 19 Jun 2001)
Revision: 3278
Log message:

      - Changed the syntax of resource implementation. Now you no longer need to
      re-declare resource types in the implementation. Instead of the declaration
      and a Mp_resource.create call, use the following syntax in the implementation:
      
      let resource <name> = <expr>
      
      where <expr> is an expression that of the type Mp_resource.info
      
      - Additionally, it is no longer necessary to use _resource in resource names
      and resource annotations.
      

Changes  Path
+5 -4 metaprl/editor/ml/package_sig.mlz
+6 -2 metaprl/editor/ml/shell_package.ml
+14 -4 metaprl/filter/base/filter_cache.ml
+3 -0 metaprl/filter/base/filter_cache.mli
+29 -33 metaprl/filter/base/filter_cache_fun.ml
+10 -6 metaprl/filter/base/filter_cache_fun.mli
+21 -0 metaprl/filter/base/filter_ocaml.ml
+6 -0 metaprl/filter/base/filter_ocaml.mli
+55 -62 metaprl/filter/base/filter_prog.ml
+6 -6 metaprl/filter/base/filter_prog.mli
+117 -123 metaprl/filter/base/filter_summary.ml
+89 -88 metaprl/filter/base/filter_summary.mli
+11 -9 metaprl/filter/base/filter_summary_type.ml
+4 -20 metaprl/filter/base/filter_summary_util.ml
+4 -8 metaprl/filter/base/filter_summary_util.mli
+9 -8 metaprl/filter/base/filter_type.ml
+7 -3 metaprl/filter/filter/filter_bin.ml
+27 -31 metaprl/filter/filter/filter_parse.ml
+19 -18 metaprl/refiner/reflib/mp_resource.ml
+18 -17 metaprl/refiner/reflib/mp_resource.mli
+16 -20 metaprl/theories/base/base_auto_tactic.ml
+2 -2 metaprl/theories/base/base_auto_tactic.mli
+8 -10 metaprl/theories/base/base_cache.ml
+1 -1 metaprl/theories/base/base_cache.mli
+16 -20 metaprl/theories/base/base_dtactic.ml
+2 -2 metaprl/theories/base/base_dtactic.mli
+17 -24 metaprl/theories/base/typeinf.ml
+3 -3 metaprl/theories/base/typeinf.mli
+8 -10 metaprl/theories/itt/itt_decidable.ml
+1 -1 metaprl/theories/itt/itt_decidable.mli
+8 -10 metaprl/theories/itt/itt_equal.ml
+1 -1 metaprl/theories/itt/itt_equal.mli
+8 -10 metaprl/theories/itt/itt_squash.ml
+1 -1 metaprl/theories/itt/itt_squash.mli
+8 -10 metaprl/theories/itt/itt_subtype.ml
+1 -1 metaprl/theories/itt/itt_subtype.mli
+16 -18 metaprl/theories/tactic/mptop.ml
+1 -1 metaprl/theories/tactic/mptop.mli
+11 -13 metaprl/theories/tactic/summary.ml
+1 -1 metaprl/theories/tactic/summary.mli
+8 -10 metaprl/theories/tactic/top_conversionals.ml
+1 -1 metaprl/theories/tactic/top_conversionals.mli