Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-01 12:58:04 -0700 (Thu, 01 Sep 2005)
Revision: 7694
Log message:
- Xin, we are no longer using "operator" = "bterm" approach (in fact, we are
no longer using explicit bterms at all - bterms are just an external concent).
- Added a configure test for htmldoc.
| Changes | Path |
| +19 -11 | metaprl/doc/OMakefile |
| +4 -10 | metaprl/theories/itt/itt_hoas_operator.ml |
| +1 -1 | metaprl/theories/itt/itt_reflection_new.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-01 13:09:46 -0700 (Thu, 01 Sep 2005)
Revision: 7695
Log message:
More on concrete operators.
| Changes | Path |
| +1 -3 | metaprl/theories/base/base_operator.mli |
| +6 -10 | metaprl/theories/itt/itt_hoas_operator.ml |
| +0 -2 | metaprl/theories/itt/itt_hoas_operator.mli |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-02 14:08:56 -0700 (Fri, 02 Sep 2005)
Revision: 7696
Log message:
Revised the text on functors.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-02 14:09:36 -0700 (Fri, 02 Sep 2005)
Revision: 7697
Log message:
Forgot these files.
| Changes | Path |
| Added | metaprl/theories/ocaml_doc/programs/setfunctor.ml |
| Properties | metaprl/theories/ocaml_doc/programs/setfunctor.ml |
| Added | metaprl/theories/ocaml_doc/programs/setfunctor2.ml |
| Properties | metaprl/theories/ocaml_doc/programs/setfunctor2.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-02 17:30:03 -0700 (Fri, 02 Sep 2005)
Revision: 7698
Log message:
*** WARNING: Breaks binary compatibility ***
Implemented the "Operator" parameters that allow imbedding reflected
"operators" into terms. This is similar to the recently introduces Shape
parameters.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-03 16:34:04 -0700 (Sat, 03 Sep 2005)
Revision: 7699
Log message:
RefineError -> RefineForceError.
| Changes | Path |
| +1 -1 | metaprl/theories/itt/itt_logic.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-03 16:40:57 -0700 (Sat, 03 Sep 2005)
Revision: 7700
Log message:
Use LexStringSet instead of StringSet in UI.
| Changes | Path |
| +6 -6 | metaprl/support/shell/package_info.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-04 20:57:18 -0700 (Sun, 04 Sep 2005)
Revision: 7701
Log message:
One unification rule that was introduced for multi-modal case
was applied too generously - similar result could be obtained
by more than one sequence of rules. Hence we were wasting some time
in unification. This commit limits that rule application to
only one case where it really needed.
| Changes | Path |
| +1 -1 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-05 10:20:34 -0700 (Mon, 05 Sep 2005)
Revision: 7702
Log message:
Made multimodal-specific rule more narrow
| Changes | Path |
| +1 -1 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-05 10:42:30 -0700 (Mon, 05 Sep 2005)
Revision: 7703
Log message:
Removed one more redundant application of the multi-modal rule.
| Changes | Path |
| +1 -1 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-05 12:59:41 -0700 (Mon, 05 Sep 2005)
Revision: 7704
Log message:
More tests
| Changes | Path |
| +6 -0 | metaprl/theories/s4lp/s4_tests.ml |
| +934 -849 | metaprl/theories/s4lp/s4_tests.prla |
Changes by: Limin Jia (ljia at CS.Princeton.EDU)
Date: 2005-09-06 07:05:35 -0700 (Tue, 06 Sep 2005)
Revision: 7705
Log message:
Add examples
Changes by: ( at unknown.email)
Date: 2005-09-06 07:05:35 -0700 (Tue, 06 Sep 2005)
Revision: 7706
Log message:
This commit was manufactured by cvs2svn to create branch
'omake_0_9_7_pre6'.
Changes by: Limin Jia (ljia at CS.Princeton.EDU)
Date: 2005-09-06 07:16:32 -0700 (Tue, 06 Sep 2005)
Revision: 7707
Log message:
Edit
| Changes | Path |
| +0 -0 | metaprl/theories/ilc/ilc_mergesort.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-06 16:24:09 -0700 (Tue, 06 Sep 2005)
Revision: 7708
Log message:
OMakefiles for omake 0.9.7
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-15 01:36:29 -0700 (Thu, 15 Sep 2005)
Revision: 7710
Log message:
Use configure for readline/ncurses.
| Changes | Path |
| +2 -11 | metaprl/OMakefile |
| +8 -3 | metaprl/mk/defaults |
| +4 -3 | metaprl/mk/make_config |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-17 03:53:44 -0700 (Sat, 17 Sep 2005)
Revision: 7713
Log message:
Changed the names of some of the "J" modules. This was necessary because OCaml
was getting confused on OS X (where the file names are not case-sensitive).
| Changes | Path |
| +4 -4 | metaprl/refiner/reflib/jall.ml |
| +2 -2 | metaprl/refiner/reflib/jordering.ml |
| +6 -6 | metaprl/refiner/reflib/jtunify.ml |
| +1 -1 | metaprl/refiner/reflib/jtypes.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-17 14:16:32 -0700 (Sat, 17 Sep 2005)
Revision: 7714
Log message:
More text for the book.
Aleksey, don't worry if this doesn't make it into the conversion.
I can copy them over afterwards.
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-09-18 16:06:21 -0700 (Sun, 18 Sep 2005)
Revision: 7715
Log message:
Added "listmem_set".
| Changes | Path |
| +31 -0 | metaprl/theories/itt/itt_list2.ml |
| +4 -0 | metaprl/theories/itt/itt_list2.mli |
| +10753 -10838 | metaprl/theories/itt/itt_list2.prla |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-19 09:58:48 -0700 (Mon, 19 Sep 2005)
Revision: 7716
Log message:
Added the svn:externals link for libmojave.
| Changes | Path |
| Properties | metaprl |
| +1 -1 | metaprl/theories/itt/OMakefile |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-19 12:25:15 -0700 (Mon, 19 Sep 2005)
Revision: 7718
Log message:
We better use svn:// for libmojave, so people can check out read-only
copies.
| Changes | Path |
| Properties | metaprl |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-19 12:38:29 -0700 (Mon, 19 Sep 2005)
Revision: 7719
Log message:
Updated the externals definition for libmojave; added an externals definition
for doc/latex/inputs.
| Changes | Path |
| Properties | metaprl |
| Properties | metaprl/doc/latex |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-19 12:46:42 -0700 (Mon, 19 Sep 2005)
Revision: 7720
Log message:
Setting mime-type "application/x-metaprl" on all the *.prla files to tell
subversion that they should not be merged.
