The Coq mailing list

[Cedric.Auger AT lri.fr]

I got an unexpected feature:
we can "fold P in P", but I am not sure
it has any meaning...

Why isn't there any way to avoid such rewriting?
Maybe it is a stupid question, but the following can
occur, and we may "loop" unexpectedly:

Goal True /\ True.
set (P := False).
fold P in *.
(* shouldn't react as it does,
   since P is no more a definition...,
   but for bigger definitions, we
   may find handy, to keep a light
   hypothesis environnement *)
split.
 (* situation A:

  P := P : Prop
  ============================
   True

  it is a piece of cake to solve it
    *)
  split.
 (* situation A:

  P := P : Prop
  ============================
   True

  we are in the same situation,
  but we want to unfold P
    *)
  unfold P in *.