Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-05-05 20:22:43 -0700 (Sun, 05 May 2002)
Revision: 3600
Log message:

      This is a branch commit that upgrades to ocaml3.04.
      
      Warning: on this branch, metaprl compiles only in byte-code.
      (See Aleksey notes below).
      
      The extra feature: there is now an apply_rewrite function
      in Top_conversionals.
      
         val : apply_rewrite : unit -> conv -> term -> term
      
      Note: always use an instance in this kind of form:
      
         let apply_rewrite = Top_conversionals.apply_rewrite ()
         - : conv -> term -> term
      
      This will (hopefully) capture all the resources at definition time.
      
      Brian: see if this works, and let me know if there are problems.
      Mp_mc_compile is updated...
      
      Aleksey:
      
         1. I don't remember exactly what you included in the upgrade to
            ocaml-3.04...  Please remind me about the features
            needed to be added to camlp4.  Also, can you try and make
            ocaml produce native code for camlp4?  We have the old problem
            with camlp4 not being configured to produce native code.
      
         2. I'm not sure about the new resource code.  To define the
            apply_rewrite function, we need to get ahold of the resources
            live at the src definition point.  I'm assuming that
            Mp_resource.extract_top () will do that--but I'm not sure.
            Question: what can we assume about Mp_resource.extract_top?
      

Changes  Path
+4 -3 metaprl-branches/ocaml_3_04/Conscript
+0 -0 metaprl-branches/ocaml_3_04/clib/Conscript
+4 -3 metaprl-branches/ocaml_3_04/editor/ml/Conscript
+1 -1 metaprl-branches/ocaml_3_04/filter/base/Conscript
+9 -3 metaprl-branches/ocaml_3_04/filter/base/filter_comment.ml
+33 -9 metaprl-branches/ocaml_3_04/filter/base/filter_hash.ml
+139 -29 metaprl-branches/ocaml_3_04/filter/base/filter_ocaml.ml
+1 -1 metaprl-branches/ocaml_3_04/filter/base/free_vars.ml
+34 -13 metaprl-branches/ocaml_3_04/filter/base/mLast_util.ml
+2 -2 metaprl-branches/ocaml_3_04/filter/boot/Conscript
+4 -0 metaprl-branches/ocaml_3_04/filter/boot/conversionals_boot.ml
+14 -0 metaprl-branches/ocaml_3_04/filter/boot/rewrite_boot.ml
+16 -0 metaprl-branches/ocaml_3_04/filter/boot/tactic_boot.ml
+12 -0 metaprl-branches/ocaml_3_04/filter/boot/tactic_boot_sig.mlz
+11 -11 metaprl-branches/ocaml_3_04/filter/filter/Conscript
+2 -2 metaprl-branches/ocaml_3_04/mk/preface
+1 -1 metaprl-branches/ocaml_3_04/refiner/reflib/Conscript
+2 -1 metaprl-branches/ocaml_3_04/theories/Conscript
+1 -1 metaprl-branches/ocaml_3_04/theories/base/Conscript
+1 -1 metaprl-branches/ocaml_3_04/theories/itt/Conscript
+2 -2 metaprl-branches/ocaml_3_04/theories/mc/Conscript
+5 -0 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.ml
+3 -3 metaprl-branches/ocaml_3_04/theories/mc/tests/Conscript
+2 -2 metaprl-branches/ocaml_3_04/theories/ocaml/Conscript
+2 -2 metaprl-branches/ocaml_3_04/theories/tactic/Conscript
+14 -1 metaprl-branches/ocaml_3_04/theories/tactic/mptop.ml
+5 -0 metaprl-branches/ocaml_3_04/theories/tactic/top_conversionals.ml
+4 -0 metaprl-branches/ocaml_3_04/theories/tactic/top_conversionals.mli
+1 -1 metaprl-branches/ocaml_3_04/util/Makefile
+26 -8 metaprl-branches/ocaml_3_04/util/macro.ml