Can one use comments in strategies?

[Tamarah Arons <tamarah@wisdom.weizmann.ac.il>]

Hello,

I have been adding comments to strategies and have come across a
problem : if I edit a proof file with comments in it from strategies 
it seems to delete the commands after the comment. This happens 
even if I just open the file for editing and then install it unchanged. 

Below is a PVS dump file with a short proof exhibiting this problem. 
It was run on PVS2-3. Using a patch does not seem to make a difference.
If you edit the proof using (M-x edit-proof), save, and then install it, 
with or without making changes, the commands after (CASEPROP) are 
replaced with NIL.

Is there some prohibition on using comments in strategies? 
Or is there some rule regarding their use that I am violating?

Thanks,
Tamarah
_________________________________________________________

$$$pvs-strategies
(defstep caseProp ()
  (then (spread (case "prop!1(seq!1, i!1)")
           ((comment "case  prop!1(seq!1, i!1)")
            (comment "case  (NOT prop!1(seq!1, i!1))")
           )
         )
   )      
  "Splits on the case that a!1(seq!1, i!1)"
  "Splits on the case that a!1(seq!1, i!1)"
)

$$$myops.pvs
myops[STATE : NONEMPTY_TYPE]: THEORY

 BEGIN

  STATE_SEQ: TYPE = [nat -> STATE]
   
  MY_PROP : TYPE = [STATE_SEQ, nat -> boolean]
 
  i,k : VAR nat
 
  e, f : VAR STATE

  seq : VAR STATE_SEQ

  prop, prop2 : VAR MY_PROP

  NOT : [MY_PROP -> MY_PROP] =  (lambda prop : (lambda seq, i: not prop(seq, i)));

  IMPLIES : [MY_PROP, MY_PROP -> MY_PROP] =  
        (lambda prop, prop2: (lambda seq, i: not prop(seq, i) or prop2(seq, i)));

  AND : [MY_PROP, MY_PROP -> MY_PROP] =  
        (lambda prop, prop2: (lambda seq, i: prop(seq, i) and prop2(seq, i)));

  G :  [MY_PROP -> MY_PROP] = (lambda prop : (lambda seq, i: FORALL k: k >= i IMPLIES prop(seq, k)));

  valid : [MY_PROP -> bool] =
     (lambda prop : forall seq, i : prop(seq, i))

  test : lemma
    forall prop: valid(G(prop) implies (prop and not not prop))

 END myops


$$$myops.prf
(|myops|
 (|test| "" (EXPAND "valid")
  (("" (EXPAND "G")
    (("" (EXPAND "implies")
      (("" (SKOSIMP*)
        (("" (EXPAND "and")
          (("" (CASEPROP)
            (("1" (EXPAND "not") (("1" (ASSERT) NIL NIL))
              ";;;case  prop!1(seq!1, i!1)")
             ("2" (INST? -) (("2" (ASSERT) NIL NIL))
              ";;;case  (NOT prop!1(seq!1, i!1))"))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))