Skip to Content.
Sympa Menu

coq-club - [Coq-Club] I am completely befuddled by this error message.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] I am completely befuddled by this error message.


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page