Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-05-01 14:25:45 -0700 (Sun, 01 May 2005)
Revision: 7240
Log message:

      Update to match libmojave.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-01 19:22:14 -0700 (Sun, 01 May 2005)
Revision: 7241
Log message:

      - Use omake's internal digest function for magic number computation in
        filter/base
      
      - Stripped the "0x" prefix from the MD5 sum comment in filter_magic.ml (I
        could have easily preserve it in the new setup, I just desided that it does
        not make sense to keep it).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-02 03:57:53 -0700 (Mon, 02 May 2005)
Revision: 7242
Log message:

      Give an error message reading "not enough information to infer the type of the
      hypothesis - v: t" instead of a very cryptic "unbound variable -
      'sequent-hypNNNN".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-02 04:52:52 -0700 (Mon, 02 May 2005)
Revision: 7243
Log message:

      When a free variable is encountered where a hypothesis type is expected, just
      unify it with "TypeHyp (gensym(), gensym ())" instead of giving up.
      
      Jason, please take a look - is this reasonable?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-02 19:22:20 -0700 (Mon, 02 May 2005)
Revision: 7244
Log message:

      Attempt and making the ASCII syntax documentation a bit more clear.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-05-02 20:41:49 -0700 (Mon, 02 May 2005)
Revision: 7245
Log message:

      removed references to Cic_ind_elim!prodH (which does nto exist)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-04 15:27:35 -0700 (Wed, 04 May 2005)
Revision: 7246
Log message:

      Ignore .omakedb.lock
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-05 15:12:53 -0700 (Thu, 05 May 2005)
Revision: 7247
Log message:

      Updated to support more browsers.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-05 15:18:56 -0700 (Thu, 05 May 2005)
Revision: 7248
Log message:

      Adding a missing line to the HOSC paper.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-05 16:09:30 -0700 (Thu, 05 May 2005)
Revision: 7249
Log message:

      Renamed Ocaml!OCaml -> Ocaml!TyOCaml (to avoid clashes with Comment!OCaml).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-05 16:10:11 -0700 (Thu, 05 May 2005)
Revision: 7250
Log message:

      Fixed a display form that broke recently.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-05-05 20:40:11 -0700 (Thu, 05 May 2005)
Revision: 7251
Log message:

      removed "stray" prodH declaration
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-05-05 21:38:35 -0700 (Thu, 05 May 2005)
Revision: 7252
Log message:

      Some fixes in display forms
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-06 16:35:50 -0700 (Fri, 06 May 2005)
Revision: 7253
Log message:

      Removing itt_eq_base - this idea did not work out.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-05-06 21:57:23 -0700 (Fri, 06 May 2005)
Revision: 7254
Log message:

      Typing of induction elimination operation (primitive recursion) is complete
      Conversions are to come.
      

Changes by: ( at unknown.email)
Date: 2005-05-06 21:57:23 -0700 (Fri, 06 May 2005)
Revision: 7255
Log message:

      This commit was manufactured by cvs2svn to create branch 'new_scanner2'.

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-05-07 22:35:40 -0700 (Sat, 07 May 2005)
Revision: 7256
Log message:

      First approximation of conversion rule for (primitive) recursion operation.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-05-08 16:19:19 -0700 (Sun, 08 May 2005)
Revision: 7257
Log message:

      Changes to match the scanner changes in omake.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-05-10 14:25:43 -0700 (Tue, 10 May 2005)
Revision: 7259
Log message:

      Removed the PRLFiles function.  For now, directories that have a mix
      of normal/MetaPRL .ml files (support/tactics, support/shell, theories/itt)
      use the "export rules" hack.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-05-10 17:07:05 -0700 (Tue, 10 May 2005)
Revision: 7260
Log message:

      New method for computing theories.dir and mldebug.dir (the search
      paths).
      
      If you want to add directory "-I foo" to theories.dir, add a dependency:
      
          $(THEORIES_PATH): foo
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-11 23:14:16 -0700 (Wed, 11 May 2005)
Revision: 7261
Log message:

      Removing some leftover Phobos stuff.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-11 23:25:18 -0700 (Wed, 11 May 2005)
Revision: 7262
Log message:

      A "uniformity" pass over the OMakefiles:
      
      - Turned the file lists into arrays (except when bug 475 makes it hard)
      
      - Turned "tab" symbols into spaces
      
      - Inlined the "Files" files that were only included once.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-12 00:21:54 -0700 (Thu, 12 May 2005)
Revision: 7263
Log message:

      Added  <=>  input shortcut for "iff".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-12 00:57:30 -0700 (Thu, 12 May 2005)
Revision: 7264
Log message:

      ToploopIgnoreError/ToploopIgnoreExn should not cause the http server to die.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-12 01:57:03 -0700 (Thu, 12 May 2005)
Revision: 7265
Log message:

      The exception wrappers in filter_exn and refine_exn were turning all
      exceptions into ToploopIgnoreExn (this is a fairly recent thing added by
      Jason). However, it is wrong to blindly turn a RefineError into
      ToploopIgnoreExn (since things like "expand" havily depend on RefineError's
      staying RefineErrors). To address this, I changed tghe wrapper to check
      whether the exception they just printed is a RefineError and if it is, then
      raise RefineError(ToploopIgnoreError) instead of the ToploopIgnoreExn.
      
      P.S. This "fixes" 3 proofs (they were complete, but had "junk" in them that
      caused "expand" to abort).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-12 01:57:55 -0700 (Thu, 12 May 2005)
Revision: 7266
Log message:

      Adding the image type.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-12 02:44:50 -0700 (Thu, 12 May 2005)
Revision: 7267
Log message:

      Derived the union type from the image type.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-12 15:35:19 -0700 (Thu, 12 May 2005)
Revision: 7268
Log message:

      Fixed a build issue caused by an empty [OPT]THREADSLIB variable in an array,
      when threads are disabled.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-05-12 16:10:29 -0700 (Thu, 12 May 2005)
Revision: 7269
Log message:

      This is an update to match the recent changes to omake.  This is
      mainly a change to use explicit :scanner: dependencies.
      
      The omake log message was as follows.
      
      ------------------------------------------------------------------------
      
      This is a significant change to .SCANNER rules, where .SCANNER rules
      are treated much more like normal rules.
      
      Externally, a .SCANNER rule has the usual rule form:
      
         .SCANNER: target: dependencies...
            ...scanner commands...
      
      In this commit, the scanner target is now decoupled from the
      build target, allowing a scanner result to be used for multiple
      build targets.  For example, ocamldep produces dependencies
      for .cmo and .cmx files simultaneously.  They can share
      the scanner rule by specifying an explicit :scanner: dependency.
      
          .SCANNER: scan-ocaml-%.ml: %.ml
              ocamldep $<
      
          %.cmo: %.ml :scanner: scan-ocaml-%.ml
              $(OCAMLC) ...
      
          %.cmx %.o: %.ml :scanner: scan-ocaml-%.ml
              $(OCAMLOPT) ...
      
      The current convention is that scanner targets should be named
      scan-<language>-<source-file>.
      
         -- If a rule has multiple :scanner: dependencies, the actual
            dependencies will be the union of the scanner results.
      
         -- The .SCANNER targets use a different namespace than
            normal targets, so it is valid to have overlapping rules.
      
                .SCANNER: foo:
                    echo "foo: boo"
      
                foo: :scanner: foo
                    ...
      
         -- For backwards compatibility, if a rule has no :scanner:
            dependencies, then omake will try to find a scanner with
            the same name as the target.  So in the example above,
            the :scanner: foo is actually unnecessary.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-12 16:15:10 -0700 (Thu, 12 May 2005)
Revision: 7270
Log message:

      Moved list_max from Itt_nat into Itt_list2.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-12 17:57:29 -0700 (Thu, 12 May 2005)
Revision: 7271
Log message:

      - Fixed a few minor OMakefile issues left over from the new_scanner branch
        merge.
      
      - The default SCANNER_MODE for MetaPRL is "error"
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-05-12 18:05:39 -0700 (Thu, 12 May 2005)
Revision: 7272
Log message:

      For some reason, we never exported the Win32 anti-configuration
      variables.  Perhaps we should just remove them.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-05-12 18:09:07 -0700 (Thu, 12 May 2005)
Revision: 7273
Log message:

      Removed some Win32-specific variables that are no longer needed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-12 19:02:58 -0700 (Thu, 12 May 2005)
Revision: 7274
Log message:

      No need to shadow scan-ocaml-* rules with almost identical one (we used to
      have to do this because of the .ppo, but this is no longer necessary).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-12 19:43:29 -0700 (Thu, 12 May 2005)
Revision: 7275
Log message:

      Itt_nat.nat_is_int needed an nth_hyp annotation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-13 13:08:06 -0700 (Fri, 13 May 2005)
Revision: 7276
Log message:

      Ignore .omakedb.lock on realclean.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-13 13:54:53 -0700 (Fri, 13 May 2005)
Revision: 7277
Log message:

      Added a theory of abstract operators for HOAS.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-13 22:48:39 -0700 (Fri, 13 May 2005)
Revision: 7279
Log message:

      Added a theory of the basic purely computational HOAS
      (bind/mk_term/subst/weak_dest_bterm)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-16 16:15:00 -0700 (Mon, 16 May 2005)
Revision: 7280
Log message:

      I added a HACK to make it unnecessary to type ";;" all the time on the CLI:
      
      Unless MetaPRL is running with a -batch flag, the readline call in shell_state
      will automatically append a ";;" at the end of the stdin string, unless it
      ends with a "\".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-16 18:17:20 -0700 (Mon, 16 May 2005)
Revision: 7281
Log message:

      Updated the previous "NL -> ;;" hack so that it does not attemt to add the
      ";;" to lines that already end with a ";;".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-16 20:31:08 -0700 (Mon, 16 May 2005)
Revision: 7282
Log message:

      Committed a wrong thing, please ignore the previous commit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-16 20:36:03 -0700 (Mon, 16 May 2005)
Revision: 7283
Log message:

      - Added Itt_list2.insert_at for inserting an element into a list at the
      specified location.
      
      - Made the nth_hyp resource annotation slightly smarter.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-16 21:36:15 -0700 (Mon, 16 May 2005)
Revision: 7284
Log message:

      Added a theory of "vector bindings". I still have to prove couple of theorems
      (I only proved the trivial ones so far), and may be add a few more theorems.
      
      Also, I've fixed the display form for conditional rewrites (which was wrong
      when # of conditions <> 1).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-17 02:02:41 -0700 (Tue, 17 May 2005)
Revision: 7285
Log message:

      Forgot the .prla
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-17 05:58:04 -0700 (Tue, 17 May 2005)
Revision: 7286
Log message:

      TeX fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-17 07:14:14 -0700 (Tue, 17 May 2005)
Revision: 7287
Log message:

      Ignore *.fls
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-17 07:22:41 -0700 (Tue, 17 May 2005)
Revision: 7288
Log message:

      Clean *fls
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-17 07:56:44 -0700 (Tue, 17 May 2005)
Revision: 7289
Log message:

      More minor TeX-related fixes.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-17 12:29:52 -0700 (Tue, 17 May 2005)
Revision: 7290
Log message:

      Proved a theorem in itt_hoas_vector.
      But this proof depends on the theorem /itt/itt_fun2/fun_sqeq_intro
      I don't know how to prove this theorem. Is it true?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-17 15:17:06 -0700 (Tue, 17 May 2005)
Revision: 7291
Log message:

      Proved all the Itt_fun2 theorems (removing the lambda-sqeq stuff).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 00:14:45 -0700 (Thu, 19 May 2005)
Revision: 7292
Log message:

      Slightly changing the way conditional rewrites are handled (this supposed to
      make the bound variable handling slightly more precise).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 00:35:10 -0700 (Thu, 19 May 2005)
Revision: 7293
Log message:

      Removed a bit of unused code
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 00:44:26 -0700 (Thu, 19 May 2005)
Revision: 7294
Log message:

      The apply_var_fun_[arg_]at_addr functions were not always handling sequent
      bindings correctly, fixing.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 01:14:56 -0700 (Thu, 19 May 2005)
Revision: 7295
Log message:

      Updated couple of proofs a bit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 02:36:04 -0700 (Thu, 19 May 2005)
Revision: 7296
Log message:

      Minor fixes
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 02:37:23 -0700 (Thu, 19 May 2005)
Revision: 7297
Log message:

      Print "empty" variables as "_".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 08:20:38 -0700 (Thu, 19 May 2005)
Revision: 7298
Log message:

      Minor clean-up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 09:47:15 -0700 (Thu, 19 May 2005)
Revision: 7299
Log message:

      Free var restriction on SO variables should be more conservative (should only
      apply to the body of the SO var, but not to its arguments).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 09:53:46 -0700 (Thu, 19 May 2005)
Revision: 7300
Log message:

      Fixed a conversion mismatch.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 10:19:25 -0700 (Thu, 19 May 2005)
Revision: 7301
Log message:

      Non-sequent contexts (issue 384) - fully implemented the "simple" case
      (non-sequent contexts with a "hole" argument, but no "extra" arguments).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 10:41:52 -0700 (Thu, 19 May 2005)
Revision: 7302
Log message:

      Fixed couple of places in JProver where terms were being compared with
      Pervasives.equal!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 11:26:25 -0700 (Thu, 19 May 2005)
Revision: 7303
Log message:

      Fixing another encoding/decoding mismatch.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 19:03:16 -0700 (Thu, 19 May 2005)
Revision: 7304
Log message:

      Debug printout of summary items - some items were printed with a newline at
      the end, some were not. Made sure all of them end with a \n for consistency.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 21:38:32 -0700 (Thu, 19 May 2005)
Revision: 7305
Log message:

      Use Lm_symbol.eq instead of (=) more consistently.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 22:31:05 -0700 (Thu, 19 May 2005)
Revision: 7306
Log message:

      Use proper Lm_num functions for comparing the nums (instead of
      Pervasives.compare).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-20 03:41:32 -0700 (Fri, 20 May 2005)
Revision: 7307
Log message:

      Fixed a number of places where comparisons functions from Pervasives were used
      on inappropriate data types (specifically - types containing terms and/or
      Lm_num nums).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-20 05:48:17 -0700 (Fri, 20 May 2005)
Revision: 7308
Log message:

      More fixed related to improper usage of Pervasives.compare, =, etc.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-21 15:02:34 -0700 (Sat, 21 May 2005)
Revision: 7309
Log message:

      A few fixes relating to handling and display of non-sequent contexts.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-21 16:17:49 -0700 (Sat, 21 May 2005)
Revision: 7310
Log message:

      Removing an unused module
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-21 19:23:24 -0700 (Sat, 21 May 2005)
Revision: 7311
Log message:

      Finished the Vector HOAS proofs.
      
      Added a limited form of "third order" rewriting to substT.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-22 13:57:44 -0700 (Sun, 22 May 2005)
Revision: 7312
Log message:

      Documentation fixes:
      
       - A lot of spelling fixes
      
       - Let omake know that MP_DEBUG=spell implies dependency on lib/words
      
       - When building the lib/english_dictionary.dat, build it in a temporary file
         first, followed by a rename to make it possible to run several instances
         of filter-spell in parallel.
      
       - A number of extra "doc docoff" added around display forms "let resource +="
         and other similar items
      
       - A few display form fixes.
      
       - Made the pages in the all-theories file wider.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-22 16:13:29 -0700 (Sun, 22 May 2005)
Revision: 7313
Log message:

      Fixing Yegor's Win32 issue (the usage of "$(file...)" caused a "/" vs "\"
      mismatch in a 3-place implicit rule).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-22 20:21:21 -0700 (Sun, 22 May 2005)
Revision: 7314
Log message:

      Basic deBruijn representation.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-05-22 21:17:00 -0700 (Sun, 22 May 2005)
Revision: 7315
Log message:

      I had this on win32:
      ------
      build editor\ml .test-metaprl-startup
      + echo | ./mpopt.bat -batch
      '.' is not recognized as an internal or external command,
      operable program or batch file.
      *** omake: 4086/4185 targets are up to date
      *** omake: failed (12.8 sec, 0/888 scans, 1/1982 rules, 1/5523 digests)
      *** omake: targets were not rebuilt because of errors:
         editor\ml\.test-metaprl-startup
            depends on: editor\ml\mpconfig
            depends on: editor\ml\mpopt.bat
      --------
      
      Apprently it does not like "./", so I use ".\" for win32
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-22 21:45:36 -0700 (Sun, 22 May 2005)
Revision: 7316
Log message:

      Follow-up to Yegor's change: just use the DIRSEP variable.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-22 23:22:12 -0700 (Sun, 22 May 2005)
Revision: 7317
Log message:

      Added the enforcement of non-recursivity of definitions (i.e. of the fact that
      the shape being define can not occur on the RHS of the definition) to the
      refiner.
      
      Note: this used to be enforced by the filter, but now that filter allows
      omiting from .ml declarations that are already present in .mli,
      non-recursivity is no longer enforced by the filter. And in any case, this is
      a correctness issue, so it should be enforced by the refiner.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-23 01:15:33 -0700 (Mon, 23 May 2005)
Revision: 7318
Log message:

      Defined list_of_fun (based on partial commented out definition that already
      existed) and proved a bunch of its properties.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-23 01:51:54 -0700 (Mon, 23 May 2005)
Revision: 7319
Log message:

      Working on defining bterm destructors. It's not immediatelly obvious how to
      prove nth_subterm_id, leaving it till tomorrow.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-23 11:20:17 -0700 (Mon, 23 May 2005)
Revision: 7320
Log message:

      Fixing a bug that caused problems building book2.dvi
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-05-23 13:05:36 -0700 (Mon, 23 May 2005)
Revision: 7321
Log message:

      Removed the DIRSEP.  But I can't figure out where this variable
      was defined...  Maybe Yegor had it defined in his environment?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-23 14:12:58 -0700 (Mon, 23 May 2005)
Revision: 7322
Log message:

      Added a notion of vector-substitution (substitution of a list of terms for the
      first length{tl} variables of a bound term)
      
      Improved the "third order rewriting" tactics a bit.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-05-23 16:04:45 -0700 (Mon, 23 May 2005)
Revision: 7323
Log message:

      The problem with exporting back to the parent is fixed by
      
      http://cvs.cs.cornell.edu:12000/commitlogs/omake/2005-05.html#05/05/23.19:01:46
      
      Removing the "return 0" that were acting as a workaround.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-23 20:09:37 -0700 (Mon, 23 May 2005)
Revision: 7324
Log message:

      - Bumping the OMakeVersion number (I've waited at least 20 minutes trying to
        figure out why MetaPRL was failing to build for me!)
      
      - Fixing the <:con< >> grammar a bit (in <:con< foo{bar{...}} >> it used to
        think that "bar" was a bound variable and insisted on having a "." or a ","
        after it.
      
      - Removing the unused "SLASH" variable.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-23 22:46:50 -0700 (Mon, 23 May 2005)
Revision: 7325
Log message:

      Finished proving properties of the "subterms" operator.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-24 21:46:51 -0700 (Tue, 24 May 2005)
Revision: 7326
Log message:

      Itt_omage was using Hashtbl.hash for computing hash values of _terms_. This,
      obviously, has huge potential for problems (as delayed substitutions get
      expanded, free variables computed, etc). I am hoping this would finally
      explain the weird behavior of omegaT that I have been unable to track for
      almost a week.
      
      P.S. Term_hash_code still uses Hashtbl.hash for hashing parameters (which
      include nums) and Itt_omega still uses Hashtbl.hash for hashing Ring.ring
      arrays (which may also include nums).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-25 01:49:28 -0700 (Wed, 25 May 2005)
Revision: 7327
Log message:

      Numerous documentation fixes:
      
       - MP_DEBUG=spell fixes (MP_DEBUG=spell finally compiles again)
      
       - Now docoff/junk/docon sequence does not introduce empty vertical space
      
       - Removed the old reflection theories from the theories.pdf, replacing them
         with the new itt_hoas_* theories.
      
       - Chaged so that any TeX printout of a module always starts in the "docoff"
         mode. This makes it unnecessary to always terminate documented modules in
         the "docoff" mode.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-25 05:35:40 -0700 (Wed, 25 May 2005)
Revision: 7328
Log message:

      Updated the "sequentialization of rewrtites" hack so that when it creates
      "H >- t1 ~ t2" out of "t1 <--> t2" it would also add "H" to the context
      bindings lists of all the variables in t1 and t2.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-25 05:50:15 -0700 (Wed, 25 May 2005)
Revision: 7329
Log message:

      In my previous commit, I accidentally included some temporary transition code,
      reverting.
      
      Also, it turned out that the itt_record_renaming.prla used to be malformed (it
      had two different entries called "x" - variable 'x<||>[] and Itt_labels!x) as
      a rusult of previous manual edit. Now that the file was modified, this made
      the problem explicit. Fixing...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-25 07:32:16 -0700 (Wed, 25 May 2005)
Revision: 7330
Log message:

      Defined the dest_term operator and proved the basic properties.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-25 07:54:40 -0700 (Wed, 25 May 2005)
Revision: 7331
Log message:

      Earlier today, a few .prla files got corrupted and three commits back I've
      committed a number of corrupted .prla files, so now I am committing corrected
      ones.
      
      The files were probably corrupted because of the weak memo bug. I've found
      that meta_term header comparison was missing a case - not sure if this could
      have caused the problems we were seeing, but hopefully this will finally get
      rid of them!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-25 19:45:40 -0700 (Wed, 25 May 2005)
Revision: 7332
Log message:

      A few fixes in the srec type.
      
        One of the rules was a bit too strong; replaced with a weaker derived rule.
      
        Display forms - minor fix.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-26 15:52:27 -0700 (Thu, 26 May 2005)
Revision: 7333
Log message:

      -Rename depth -> bdepth
      -Added theory hoas_bterm. I'working on proofs now
      -Added some iforms
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-27 18:06:27 -0700 (Fri, 27 May 2005)
Revision: 7334
Log message:

      More proofs
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-27 20:11:16 -0700 (Fri, 27 May 2005)
Revision: 7335
Log message:

      More proofs
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-28 00:19:27 -0700 (Sat, 28 May 2005)
Revision: 7336
Log message:

      more proofs
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-28 06:14:07 -0700 (Sat, 28 May 2005)
Revision: 7337
Log message:

      more proofs
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-28 15:40:36 -0700 (Sat, 28 May 2005)
Revision: 7338
Log message:

      The scoping testing for conditional rewrites was doing a wrong thing for
      rewriting on assumptions.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-29 14:17:03 -0700 (Sun, 29 May 2005)
Revision: 7339
Log message:

      Corrected some theorems
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-30 00:17:33 -0700 (Mon, 30 May 2005)
Revision: 7340
Log message:

      The rule  tunionElimination_eq had unfinished proof. I removed it from the elimination resource. I added the rule  tunionElimination_sq instead
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-30 00:36:16 -0700 (Mon, 30 May 2005)
Revision: 7341
Log message:

      more proofs
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-30 00:55:07 -0700 (Mon, 30 May 2005)
Revision: 7342
Log message:

      Finished proofs in itt_hoas_bterm
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-30 18:31:59 -0700 (Mon, 30 May 2005)
Revision: 7343
Log message:

      Filled in a missing proof. Now all the Itt_hoas_bterm rules have fully
      grounded proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-30 19:12:37 -0700 (Mon, 30 May 2005)
Revision: 7344
Log message:

      Minor formatting fixes