coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Error: in _: eq not found.
- Date: Fri, 2 Aug 2013 12:55:52 -0700
Hi,
What does it mean when I get the error "Error: in _: eq not found." on "rewrite foo"? (This is at https://github.com/JasonGross/HoTT-categories/blob/grothendieck-cat-partial/theories/Grothendieck/ToCat.v#L168, using the latest version of HoTT/coq.)
Thanks,
Jason
- [Coq-Club] Error: in _: eq not found., Jason Gross, 08/02/2013
Archive powered by MHonArc 2.6.18.