Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 12:37:34 -0800 (Wed, 19 Feb 2003)
Revision: 4092
Log message:

      This should finish off quotations... I have enabled term/ext quotations
      in terms, so now you can write
      
      sequent [m] { 'H >- <<AtomInt[1:n]>> }
      sequent [m] { 'H >- <:term<....>> }
      sequent [m] { 'H >- <:ext<let t = 1 in let u = 2 in u*t>> }
      
      and of course you can still use
      
      sequent [m] { 'H >- $"let t = 1 in let u = 2 in u*t"$ }
      
      The key part that we were missing was the fact that there is a token
      type QUOTATION.
      

Changes	Path
+24 -5	metaprl/filter/filter/filter_parse.ml
+0 -4	metaprl/filter/phobos/filter_phobos.ml