Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-01 00:04:52 -0800 (Tue, 01 Feb 2005)
Revision: 6554
Log message:

      Use silent mode, when VERBOSE is _false_, not when it's _undefined_ (but if it
      is undefined, set it to false).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-01 03:44:55 -0800 (Tue, 01 Feb 2005)
Revision: 6555
Log message:

      d_apply_equalT should not be topval
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-01 03:55:48 -0800 (Tue, 01 Feb 2005)
Revision: 6556
Log message:

      When Stdpp.Exc_located is raised and the file name is empty (as it happens,
      for example, with Stdpp.Exc_located exceptions raised on the CLI), there is no
      need to print the empty file name.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-01 06:51:21 -0800 (Tue, 01 Feb 2005)
Revision: 6557
Log message:

      Deleted some unused code
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-01 11:36:33 -0800 (Tue, 01 Feb 2005)
Revision: 6558
Log message:

      Changed the indentation of begin-end blocks.
      
      let x = begin
         if true then begin
            1;
            begin
               2;
               3
            end;
            4
         end
         else
            2
      end
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-01 15:07:59 -0800 (Tue, 01 Feb 2005)
Revision: 6560
Log message:

      The context_vars function makes more sense in TermMan, then in TermSubst.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-02-01 16:51:43 -0800 (Tue, 01 Feb 2005)
Revision: 6561
Log message:

      Add a theory Itt_synt_bterm
      Aleksey, note that we have to add the rule  operatorSquiddle.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-02-01 18:27:43 -0800 (Tue, 01 Feb 2005)
Revision: 6562
Log message:

      More on reflection
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-02-02 00:06:52 -0800 (Wed, 02 Feb 2005)
Revision: 6563
Log message:

      proofs.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-02-02 00:36:23 -0800 (Wed, 02 Feb 2005)
Revision: 6564
Log message:

      fixed a small bug
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-02 03:06:01 -0800 (Wed, 02 Feb 2005)
Revision: 6565
Log message:

      Whew, mmc now compiles with full type information.
      
      Here are some tradeoffs.
      
         1. Type information is *very* useful.  I caught many errors
            in mmc with it.
         2. It also requires you be more verbose.  For example, you
            might need separate terms:
      
               Foo{'e : Exp}
               FooList{'el : List{Exp}}
      
            you probably got away with just Foo{'a} before.
         3. It is also unsound.  This is mainly because there is no relation
            between rules, so one rule can't tell any type constraints of
            another rule.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-02 13:43:35 -0800 (Wed, 02 Feb 2005)
Revision: 6566
Log message:

      The standalone libmojave was forgetting all INCLUDES, so
      ssl was not being included on Win32.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-02-02 15:40:17 -0800 (Wed, 02 Feb 2005)
Revision: 6567
Log message:

      Add the connection between synt_bterm and base_reflection 'numerals'
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-02-02 15:55:38 -0800 (Wed, 02 Feb 2005)
Revision: 6568
Log message:

      proofs.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-02-02 16:03:00 -0800 (Wed, 02 Feb 2005)
Revision: 6569
Log message:

      Forget to commit base_reflection last time
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-02 17:30:13 -0800 (Wed, 02 Feb 2005)
Revision: 6570
Log message:

      Minor updates
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-02-02 18:18:11 -0800 (Wed, 02 Feb 2005)
Revision: 6571
Log message:

      made bterm_elim primitive and bterm_ind_wf interactive.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-02 22:28:40 -0800 (Wed, 02 Feb 2005)
Revision: 6572
Log message:

      Removing an unused opname
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-02 23:39:02 -0800 (Wed, 02 Feb 2005)
Revision: 6573
Log message:

      Made the interface slightly more specific
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 00:34:46 -0800 (Thu, 03 Feb 2005)
Revision: 6574
Log message:

      This brings the support for non-sequent contexts one step closer. Now the
      non-sequent contexts are properly recognized by the filter and the
      corresponding address arguments are properly recognized and properly passed to
      the rewriter.
      
      The rewriter support, however, is still incomplete (this is the last missing
      piece of the puzzle) - any non-trivial usage of contexts is likely to result
      in Invalid_argument("...not supported...") from the rewriter.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 00:41:07 -0800 (Thu, 03 Feb 2005)
Revision: 6575
Log message:

      Do not include the tests directory, unless any test files are actually in use.
      

Changes by: ( at unknown.email)
Date: 2005-02-03 00:41:07 -0800 (Thu, 03 Feb 2005)
Revision: 6576
Log message:

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

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-03 00:47:35 -0800 (Thu, 03 Feb 2005)
Revision: 6577
Log message:

      1. Strip type constraints at parse time after type checking.
      
         I added the function Term_man_{ds,gen}.sweep_up_term.
         I'm not sure, but this is probably not definable in
         Refiner_debug, because the type
      
            sweep_up_term : (term -> term) -> term -> term
      
         contains a positive occurrence of the term type in an argument.
      
         We *could* move this function out of the refiner, but it
         seems a bit silly to do it.  Let's see what Aleksey thinks.
      
      2. I accidentally removed collect_opnames in Filter_cache_fun.
         Added it back.
      
      check-status now works, apart from the new theorems for reflection.
      It is time to merge, at least once we decide what to do with the
      sweep_up_term function.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 01:51:30 -0800 (Thu, 03 Feb 2005)
Revision: 6578
Log message:

      The display form operators ("slot", "pushm", etc) and options ("mode",
      "parens", etc) are now properly declared in the Perv module instead of being
      hacked into the opname table by the Filter_cache_fun. (Issue 398)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 02:03:33 -0800 (Thu, 03 Feb 2005)
Revision: 6579
Log message:

      Display forms updates to support the recently added address parameters.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 03:57:02 -0800 (Thu, 03 Feb 2005)
Revision: 6580
Log message:

      Removing TermMan.sweep_up_term (which was a dup of TermOp.map_up_term)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 04:03:27 -0800 (Thu, 03 Feb 2005)
Revision: 6581
Log message:

      It's map_up, not map_up_term, sorry!
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-03 11:08:01 -0800 (Thu, 03 Feb 2005)
Revision: 6582
Log message:

      Ported the display form changes, and removed the wildcard types
      for unknown terms.
      
      Added types for quoted terms.  For example if we have
      
         declare lambda{x : T1. 'e['x] : T2} : T3
      
      then we also get
      
         lambda[@]{x : Term. Term} : Term
      
      I would rather use a type Quote for quoted terms, but this will
      surely break in ITT.  For example, the following would be
      well-typed:
      
         apply[@]{t1[@]; t2[@]}
      
      but the following would break
      
         apply[@]{fst{pair{t1[@]; t0[@]}}; t2[@]}
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 12:25:54 -0800 (Thu, 03 Feb 2005)
Revision: 6583
Log message:

      Fixing TERMS=std
      

Changes by: ( at unknown.email)
Date: 2005-02-03 12:25:54 -0800 (Thu, 03 Feb 2005)
Revision: 6584
Log message:

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

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-03 16:00:47 -0800 (Thu, 03 Feb 2005)
Revision: 6586
Log message:

      Added the Quote typeclass.  Quoted terms have types like the following.
      
         apply[@]{'t1 : Term; 't2 : Term} : Quote
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 18:14:03 -0800 (Thu, 03 Feb 2005)
Revision: 6587
Log message:

      Yet another instance of the opname_classes branch, merged once again with the
      trunk changes and re-branched.
      
      Known issues:
       - The .mli opname declarations are added to the .cmoz in the reverse order.
         This, among other things causes Failure ("unknown typeclass:
         Mmc_base_judgment!Prop") exception on cd'ing into the /mmc_base_judgment
         module.
       - The .mli opname declarations are added to the .cmoz even when .cmoz has its
         own copy. That results in the "ls" output (and other things, such as .cmoz
         and .prla files) being unnecessarily cluttered.
       - If the same shape is declared several times (possibly with incompatible
         types), does anybody notice?
      
      Potential TODOs and RFEs:
       - Proper type checking for display forms.
       - Could we may be come up with a way to propagate certain declarations from
         .ml into .cmiz (instead of the other way around)? Some declarations needs
         to stay in the .ml in order to get properly documented.
       - "declare sequent" shortcuts:
          - when the type is { Term : Term >- Term } : Term, allow omitting it
          - when the type is { Term : Term >- Term } : Foo, allow typing just ": Foo"
       - Perv!nil/Perv!cons should have the Dform type.
          - When the sequent conclusion is omitted, a we should use something other
            than Perv!nil for the conclusion. This new "default conclusion" term
            should be a member of a singleton type (in the Term typeclass), and MMC
            should be using that in the type of Mmc_core_ast!ty_args
          - Base_reflection should use its own cons and nil for bterm lists.
       - The new stuff (both the new syntax and the typechecking algorithm) need to
         be documented.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 18:15:24 -0800 (Thu, 03 Feb 2005)
Revision: 6588
Log message:

      These got accidentally resurrected in one of the merges. Removing them again.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 18:34:03 -0800 (Thu, 03 Feb 2005)
Revision: 6589
Log message:

      Annotated a few things with ": Dform"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 19:51:33 -0800 (Thu, 03 Feb 2005)
Revision: 6590
Log message:

      - Removed the obsolte "Opname" and "Definition" choices from the summary_item
        type (Filter_summary has hack that prevents it from complaining about
        unknown "opname" and "definition" items in the old .prla)
      
      - Restored the ability to have a declare+rewrite in the interface and a define
        in the implementation.
      
      - Made the ls options processor a bit smarter about the new "declare" items.
        In particular, an ordinary "declare" directive is going to be consideted
        formal when the type does not mention "Dform" and is going to be considered
        informal and display-related when it does.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-03 20:35:03 -0800 (Thu, 03 Feb 2005)
Revision: 6591
Log message:

      Copy declare items from the interface during the checking phase.
      This eliminates duplicate declares, and provides a genric way to copy
      items from the interface.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-03 21:29:29 -0800 (Thu, 03 Feb 2005)
Revision: 6592
Log message:

      Prevent redeclaration of shapes.
      
      Note that Itt_rat, Itt_rbtree had errors in this respect,
      using define more than once on the same shape.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 23:11:52 -0800 (Thu, 03 Feb 2005)
Revision: 6593
Log message:

      Adding a few "XXX BUG" comments on some of the places Jason found.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-04 09:38:16 -0800 (Fri, 04 Feb 2005)
Revision: 6594
Log message:

      Thread the flag for shape checking, rather than using an imperative
      variable.  This allows shape checking for sub-theories, and is less
      likely to cause problems in the future.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-04 12:29:12 -0800 (Fri, 04 Feb 2005)
Revision: 6595
Log message:

      Fixing the documentation display forms (that I broke when merging
      opname_classes3).
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-02-04 14:10:55 -0800 (Fri, 04 Feb 2005)
Revision: 6596
Log message:

      Fix a bug in itt_rbtrees
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-04 17:56:31 -0800 (Fri, 04 Feb 2005)
Revision: 6597
Log message:

      Improved display forms for the "declare" directives.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-04 19:41:51 -0800 (Fri, 04 Feb 2005)
Revision: 6598
Log message:

      This tries to be more careful about parsing terms.
      
      In general if you see an unparsed term in MetaPRL, it has to be
      due to the use of one of two functions being used in Filter_parse:
      raw_term_of_parsed_term, or quote_term_of_parsed_term.  These are the
      only two functions that bypass term parsing.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-04 20:22:14 -0800 (Fri, 04 Feb 2005)
Revision: 6599
Log message:

      Starting display form typing.  Removed the create_term_parser function in
      favor of a rewrite_of_parsed_rewrite function.  There is limited demand
      for user-defined parsers.  We can resurrect if necessary, but I doubt we'll
      need to.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-04 21:39:34 -0800 (Fri, 04 Feb 2005)
Revision: 6600
Log message:

      Added comments with the exact shell command lines needed to generate the code
      for the Refiner_debug submodules.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-02-05 02:32:33 -0800 (Sat, 05 Feb 2005)
Revision: 6601
Log message:

      added and proved some useful rules.
      
      Alexei, can you take a look at "all_list_elim"? It seems that we have to add sth about the wellformedness of 'P.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-05 09:43:23 -0800 (Sat, 05 Feb 2005)
Revision: 6602
Log message:

      Added a bunch of comments
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-05 17:14:46 -0800 (Sat, 05 Feb 2005)
Revision: 6603
Log message:

      Added display-form type checking.  This was a little painful because
      some theories were using xlist as a normal list.  In the end, I changed
      the declarations to the following.
      
         declare xcons{'a : Dform; 'b : Dform} : Dform
         declare xnil : Dform
      
      Base_reflection has its own list, using rcons and rnil.
      You need to use the functions mk_rlist_term, is_rlist_term, etc.,
      instead of mk_xlist_term, is_xlist_term.
      
      The .prla updates are just for the opname renaming.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-05 17:24:35 -0800 (Sat, 05 Feb 2005)
Revision: 6604
Log message:

      Added typechecking on productions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-05 18:59:00 -0800 (Sat, 05 Feb 2005)
Revision: 6605
Log message:

      squiddle -> squiggle
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-05 19:55:00 -0800 (Sat, 05 Feb 2005)
Revision: 6606
Log message:

      Disallow type constraints rules and rewrites.  For type inference,
      type rewrites become equalities.
      
         declare rewrite TyElem{TyExp} <--> Exp
      
      This means, in addition to the rewrite, that TyElem{TyExp} = Exp.
      So, if we are unifying t1 and t2, it is legal to unify t1 with TyElem{TyExp},
      and Exp with t2.
      
      >    Known issues:
      >     - The .mli opname declarations are added to the .cmoz in the reverse order.
      >       This, among other things causes Failure ("unknown typeclass:
      >       Mmc_base_judgment!Prop") exception on cd'ing into the /mmc_base_judgment
      >       module.
      >     - The .mli opname declarations are added to the .cmoz even when .cmoz has its
      >       own copy. That results in the "ls" output (and other things, such as .cmoz
      >       and .prla files) being unnecessarily cluttered.
      
      These are fixed.  Only the declarations that don't exist in the .ml are copied.
      
      >     - If the same shape is declared several times (possibly with incompatible
      >       types), does anybody notice?
      
      This is now checked in Filter_cache_fun.
      
      >    Potential TODOs and RFEs:
      >     - Proper type checking for display forms.
      
      Implemented.
      
      >     - Could we may be come up with a way to propagate certain declarations from
      >       .ml into .cmiz (instead of the other way around)? Some declarations needs
      >       to stay in the .ml in order to get properly documented.
      
      What about copying the documentation from the .mli (preserving the order)?
      
      >     - "declare sequent" shortcuts:
      >        - when the type is { Term : Term >- Term } : Term, allow omitting it
      >        - when the type is { Term : Term >- Term } : Foo, allow typing just ": Foo"
      
      Implemented.
      
      >     - Perv!nil/Perv!cons should have the Dform type.
      >        - When the sequent conclusion is omitted, a we should use something other
      >          than Perv!nil for the conclusion. This new "default conclusion" term
      >          should be a member of a singleton type (in the Term typeclass), and MMC
      >          should be using that in the type of Mmc_core_ast!ty_args
      >        - Base_reflection should use its own cons and nil for bterm lists.
      
      Implemented.
      
      >     - The new stuff (both the new syntax and the typechecking algorithm) need to
      >       be documented.
      
      I need to do this.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-06 15:21:43 -0800 (Sun, 06 Feb 2005)
Revision: 6607
Log message:

      Typechecking is now stricter.
         -- For rules and rewrites, the goal types are existentially quantified.
         -- Rewrites are type-invariant.  For example, the following will fail.
      
            declare typeclass A
            declare typeclass B -> A
            declare foo : A
            declare bar : B
      
            prim_rw bad : foo <--> bar
      
            This is rejected because the (bar --> foo) rewrite is bogus.
      
      At this point, the type system is basically sound, apart from
      rule and rewrite arguments, and assuming the implementation is
      correct.  Let's merge.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-06 16:25:59 -0800 (Sun, 06 Feb 2005)
Revision: 6608
Log message:

      Removed a bit of unused code
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-06 17:09:02 -0800 (Sun, 06 Feb 2005)
Revision: 6609
Log message:

      Term_shape_gen.term_shape type does not need to be concrete
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-06 18:52:20 -0800 (Sun, 06 Feb 2005)
Revision: 6610
Log message:

      Perv!dummy_arg is now Comment!dummy_arg and has a display form.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-06 19:33:24 -0800 (Sun, 06 Feb 2005)
Revision: 6611
Log message:

      1. Some work on mmc.
      
      2. Fixed the problem with parsed term in comments.
      > 1) The problem with <:doc< ... << ... >> ... >>
      >
      > still exists.
      
         The terms in comments are now parsed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-06 20:45:56 -0800 (Sun, 06 Feb 2005)
Revision: 6612
Log message:

      - I've added a "docon" term that is the opposite of the "docoff". One can now
        write simply
           doc docon
        instead of having to do something like
           doc <:doc< @doc{ } >>
      
      - I've added "doc docoff"/"doc docon" in a few places in ITT to exclude ML
        code from the theories.pdf file (I did this some of the theories that needed
        it, but most likely not in all of them).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-06 20:48:48 -0800 (Sun, 06 Feb 2005)
Revision: 6613
Log message:

      OCaml code uses ocons/onil, not xcons/xnil.
      This fixes the ocaml display I believe.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-06 21:10:51 -0800 (Sun, 06 Feb 2005)
Revision: 6614
Log message:

      Annotated  a lot of the "dforms helper" operators (including all in itt_comment
      and czf_itt_comment) with the "Dform" type.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-06 22:25:16 -0800 (Sun, 06 Feb 2005)
Revision: 6615
Log message:

      display_col can now be typed properly
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-06 22:44:47 -0800 (Sun, 06 Feb 2005)
Revision: 6616
Log message:

      Annotated a few more dform "helper" opname with the ": Dform" type annotation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-06 23:02:20 -0800 (Sun, 06 Feb 2005)
Revision: 6617
Log message:

      My previos changes would not actually compile, fixing.
      (Omake told me that they've compiled, but it was a lie! See bug 403).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-06 23:10:31 -0800 (Sun, 06 Feb 2005)
Revision: 6618
Log message:

      df_rev_concat needs to know about ocons/onil as well.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-06 23:15:53 -0800 (Sun, 06 Feb 2005)
Revision: 6619
Log message:

      Trivial comment change
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-06 23:57:02 -0800 (Sun, 06 Feb 2005)
Revision: 6620
Log message:

      Added support for non-sequent contexts to Term_man_ds.context_vars_info
      
      However I am still getting a type error from Itt_test.context_rw:
                   Itt_rfun!let
                       {'e1;
                        v. context[C:v]{C. 'e2['v]; Perv!xcons{'C; Perv!xnil}}}
                   - has type
                   - Perv!Term
                   - but is used with type
                   - Perv!type[C1093:v]
                   - unify_normal_term_types2
                   - term type
                   - Perv!Term - is not compatible with - Perv!type[C1093:v]
      
      The error is sort of correct - this rewrite is only type-safe when applied to
      something of type Term, while it could potentially be applied to something
      else. Jason, what do you think would be the right thing to do here? Should we
      indeed consider this illegal?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-07 00:25:47 -0800 (Mon, 07 Feb 2005)
Revision: 6621
Log message:

      Display form fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-07 01:38:16 -0800 (Mon, 07 Feb 2005)
Revision: 6622
Log message:

      Added display forms for the labels declared in Itt_labels.
      
      A better way would be to add an opname shortener to the Dforms module,
      this commit is just a workaround.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-02-07 02:34:55 -0800 (Mon, 07 Feb 2005)
Revision: 6623
Log message:

      Proved most of the rules in itt_synt_bterm.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-07 04:25:55 -0800 (Mon, 07 Feb 2005)
Revision: 6624
Log message:

      ***************************************************************************
      ****             !!!!!         WARNING            !!!!!                ****
      ***************************************************************************
      !!!!!           This commit breaks binary compatibility               !!!!!
      !!!!!         Export all your uncommitted proofs before updating      !!!!!
      !!!!!                                                                 !!!!!
      !!!!!  If you export to a .prla that did not exist before, you will   !!!!!
      !!!!!  to edit it manually after you update - find the line that      !!!!!
      !!!!!  starts with "NPerv!cons" replace the last (third) occurrence   !!!!!
      !!!!!  of "cons" with "xcons", then replace last (third) occurrence   !!!!!
      !!!!!  nil" with "xnil" on the "Perv!nil" line.                       !!!!!
      !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
      
      Merging the opname_classes branch!
      
      This commit inroduces types to MetaPRL syntax with an informal (but pretty
      precise) typechecking. Hopefully Jason will write some documentation
      describing how to use this.
      
      This fixes bug 370 and bug 371.