Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-19 23:23:30 -0800 (Fri, 19 Mar 2004)
Revision: 5501
Log message:

      - Finished implementing an Mp_resource-based dforms management mechanism.
      - Updated support/shell to use the new API.
      

Changes	Path
+34 -1	metaprl-branches/new_match_table/refiner/reflib/dform.ml
+10 -2	metaprl-branches/new_match_table/refiner/reflib/dform.mli
+1 -1	metaprl-branches/new_match_table/support/shell/display_term.ml
+1 -1	metaprl-branches/new_match_table/support/shell/display_term.mli
+0 -2	metaprl-branches/new_match_table/support/shell/mptop.ml
+0 -11	metaprl-branches/new_match_table/support/shell/package_info.ml
+1 -3	metaprl-branches/new_match_table/support/shell/package_sig.mlz
+0 -1	metaprl-branches/new_match_table/support/shell/proof_edit.ml
+1 -2	metaprl-branches/new_match_table/support/shell/proof_edit.mli
+2 -7	metaprl-branches/new_match_table/support/shell/shell.ml
+1 -1	metaprl-branches/new_match_table/support/shell/shell_package.ml
+1 -1	metaprl-branches/new_match_table/support/shell/shell_root.ml
+1 -2	metaprl-branches/new_match_table/support/shell/shell_sig.mlz
+0 -1	metaprl-branches/new_match_table/support/shell/shell_state.ml
+0 -7	metaprl-branches/new_match_table/support/tactics/top_tacticals.ml
+0 -1	metaprl-branches/new_match_table/support/tactics/top_tacticals.mli
+4 -3	metaprl-branches/new_match_table/tactics/proof/proof_boot.ml
+3 -10	metaprl-branches/new_match_table/tactics/proof/proof_term_boot.ml