Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-03 23:48:48 -0800 (Fri, 03 Dec 2004)
Revision: 6326
Log message:

      There is no need to name individual punctuation symbols in the term grammar.
      
      Note that this no-op commit dramatically reduces the compile time for this
      file. On Mojave clients, compiling just this one file use to take about a
      minute and now it is down to less than 20 seconds!
      

Changes  Path
+75 -111 metaprl/filter/filter/term_grammar.ml