Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-30 14:21:54 -0800 (Sun, 30 Mar 2003)
Revision: 4353
Log message:

      Fixed "make latex".
      

Changes  Path
+2 -1 metaprl/theories/tactic/comment.ml