Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-07-04 16:54:21 -0700 (Tue, 04 Jul 2006)
Revision: 9418
Log message:

      Include the words file in the distribution so that we do not need to worry
      about different setups having very different words files (or no words file at
      all). This version of the words.linux file is a copy of the linux.words file
      from Red Hat's words-3.0-3 package, which in turn took the file from
      http://www.dcs.shef.ac.uk/research/ilash/Moby/.
      
      Also, removed a number of words from words.metaprl as they now appear in the
      words.linux.
      
      P.S. According to both the package and the above URL, the file is in public
      domain.
      

Changes  Path
+1 -1 metaprl/OMakefile_theories
+1 -1 metaprl/filter/OMakefile
+4 -6 metaprl/filter/base/filter_spell.ml
Deleted metaprl/filter/words
Added metaprl/filter/words.linux
Copied metaprl/filter/words.metaprl
+54 -0 metaprl/filter/words.metaprl
+9 -0 metaprl/mk/defaults

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-07-04 20:04:58 -0700 (Tue, 04 Jul 2006)
Revision: 9419
Log message:

      Simplified the spellchecker slightly.
      

Changes  Path
+14 -32 metaprl/filter/base/filter_spell.ml
+1 -1 metaprl/filter/filter/term_grammar.ml
+1 -1 metaprl/theories/czf/czf_itt_group.ml
+1 -1 metaprl/theories/itt/core/itt_pairwise.ml
+1 -1 metaprl/theories/itt/core/itt_subset.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-07-04 20:12:12 -0700 (Tue, 04 Jul 2006)
Revision: 9420
Log message:

      (Bug 594) Do not overwrite mk/config.local when it already exists.
      

Changes  Path
+3 -1 metaprl/mk/load_config
+1 -2 metaprl/mk/make_config

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2006-07-05 17:57:31 -0700 (Wed, 05 Jul 2006)
Revision: 9423
Log message:

      Use of Filename.concat instead of explicit slashes.
      
      Under win32 I get:
      
      - build support\display comment.cmoz
      + Shell.prlcomp(lib\camlp4n.exe -o comment.ppo comment.ml)
      Building spelling dictionary ..\..\lib\english_dictionary.dat...While processing
       implem:
          File "comment.ml", line 1, char 1 -- line 2130, char 1:
             Sys_error("Permission denied")
      *** omake error:
         File mk\prlcomp: line 22, characters 9-21
         command terminated with code 2: Shell.exit(2 : Int)
      
      *** omake: 2632/3384 targets are up to date
      *** omake: failed (155.0 sec, 1/573 scans, 22/1018 rules, 39/4081 digests)
      *** omake: targets were not rebuilt because of errors:
         support\display\comment.cmoz
            depends on: support\display\comment.ml
         support\display\comment.ppo
            depends on: support\display\comment.ml
      
      Permissions seem to be ok, I can do this rename form ocaml manually.
      Unix -> Sys does not help either.
      Any ideas what could be causing it?

Changes  Path
+3 -3 metaprl/filter/base/filter_spell.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-07-07 16:33:04 -0700 (Fri, 07 Jul 2006)
Revision: 9428
Log message:

      - Do not insist on being able to rename the tmp file into .dat if .dat already
        exists (Win32 fix).
      
      - Use "open" instead of "include" for the system build library.
      

Changes  Path
+3 -4 metaprl/OMakeroot
+7 -3 metaprl/filter/base/filter_spell.ml

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-07-10 17:05:54 -0700 (Mon, 10 Jul 2006)
Revision: 9436
Log message:

      A couple of theorems

Changes  Path
+15 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.ml
+3246 -2902 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.prla