The Coq mailing list

[Pierre Cast�ran <pierre.casteran AT labri.fr>]

Hi,

  I met some problems using rewrite.
  In a goal like that :

  Edges.mem (phi x, a) (E_of G') = Edges.mem (phi x, phi x0) (E_of G') ->
   Edges.mem (phi x, a) (E_of G') = true

  The sequence "intro e; rewrite e" fails with the message
  Error:
Found no subterm matching "Edges.mem (phi x, a) (E_of G')" in the current goal

I suspect that this kind of problem comes from the fact that both terms,
although equivalent, do not share the same representation (this example
comes from a development with many functor applications).

 I didn't find which command would allow me to find the differences
between the two occurrences of the term "Edges.mem (phi x, a) (E_of G') "


Pierre

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.