coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "M. Scott Doerrie" <mdoerri AT cs.jhu.edu>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] I am completely befuddled by this error message.
- Date: Wed, 24 Jun 2009 16:09:24 -0400
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] I am completely befuddled by this error message., M. Scott Doerrie
- Re: [Coq-Club] I am completely befuddled by this error message., Brian Aydemir
- Re: [Coq-Club] I am completely befuddled by this error message., Adam Chlipala
- Re: [Coq-Club] I am completely befuddled by this error message., Adam Koprowski
Archive powered by MhonArc 2.6.16.