The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

On Jun 24, 2009, at 4:09 PM, M. Scott Doerrie wrote:

> How the heck can I get this error message?  It is most confusing.
>
> 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"

The first thing I would do here is

        Set Printing All.

which prints out the raw terms---implicit arguments are explicit, no  
notations, etc.  In a situation like this, I often find that something  
normally hidden from display is causing things not to unify or match.   
(Maybe there are multiple, convertible ways of writing RefSet.t?)

I hope that helps,
Brian