Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-26 16:00:43 -0800 (Wed, 26 Feb 2003)
Revision: 4137
Log message:

      I am committing this file separately.
      I added another :desc "quotation" (for IR descriptions). Among others,
      this would be useful in rewrite rules, which expect mterms, but ideally
      we shouldn't duplicate code. So if you can figure out a better parse
      symbol to extend (so that you can use this "quotation" in sequents as well),
      feel free to revert this code. I didn't think nonwordterm was the right
      symbol to extend for this.
      

Changes	Path
+35 -1	metaprl/filter/filter/filter_parse.ml