The Coq mailing list

["M. Scott Doerrie" <mdoerri AT cs.jhu.edu>]

How the heck can I get this error message?  It is most confusing.

I will note I'm using 8.1pl4, not the recently released 8.2.  I had some 
issues with an upgrade and haven't worked it out yet.

f : R.t -> AG.t -> AG.t
f' : R.t -> AG.t -> AG.t
refs : RefSet.t
refs' : RefSet.t
acc : AG.t
acc' : AG.t
H : RefSet.Equal refs refs'
H0 : AG.Equal acc acc'
H1 : forall (r r' : R.t) (ag ag' : AG.t),
    AG.Equal ag ag' -> R.eq r r' -> AG.Equal (f r ag) (f' r' ag')
H4 : refs' = refs
The term "H4" has type "refs' = refs" while it is expected to have type
"refs' = refs"

Michael Doerrie