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)
Rev