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'.