coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Unknown exception in Scheme Equality command

From: Dominic Mulligan <dominic.p.mulligan AT googlemail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Re: Unknown exception in Scheme Equality command
Date: Mon, 19 Nov 2012 11:05:22 +0000

As a follow up on my previous message which omitted the entirety of the
output that Coq is actually giving, it appears that t_beq is being
defined, and the exception seems to occur in the generation of t_eq_dec:

t_beq is defined

Error: Unknown exception during scheme creation.

Dom

[Coq-Club] Re: Unknown exception in Scheme Equality command, Dominic Mulligan, 11/19/2012