The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Hi,

I am using FMaps in my development and want to write a tactic that
matches hypotheses of the form (MyMap.MapsTo k v m).  The problem is
that, when I destruct a proposition of the form (MyMap.In k m), I end
up with a hypothesis of the form (MyMap.Raw.PX.MapsTo _ _ _).  A
tactic that matches on (MyMap.MapsTo _ _ _) will not match hypotheses
of the form (MyMap.Raw.PX.MapsTo _ _ _).  Of course, I can write a
tactic that refers directly to MyMap.Raw.PX.MapsTo, but I feel like
this is violating the intended abstraction of the FMap interface.
Unforunately, the tactic "fold MyMap.MapsTo" does not help because
MyMap.MapsTo seems to be defined as an eta-expansion of
MyMap.Raw.PX.MapsTo.  Any other ideas?  Or do I have to write a tactic
that breaks the abstraction?

 - Aaron