The Coq mailing list

["Andrew McCreight" <continuation AT gmail.com>]

Hi,

This problem has been discussed before on the mailing list:

http://pauillac.inria.fr/pipermail/coq-club/2008/003728.html

That message has a bit of a workaround plus a link to the (not very useful) bug report in the Coq bug database.

-Andrew

On Wed, Jul 30, 2008 at 10:07 AM, <Cedric.Auger AT lri.fr> wrote:

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 *.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club