# Can one use comments in strategies?

```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 ()
((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))

```