coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Explanation of setoid_rewrite "Error: build_signature: no constraint can apply on a dependent argument"

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Explanation of setoid_rewrite "Error: build_signature: no constraint can apply on a dependent argument"
Date: Mon, 24 Dec 2012 17:35:22 -0500

Hi,

Can someone explain to me, or point me to an explanation of, the setoid_rewrite "Error: build_signature: no constraint can apply on a dependent argument"?

(If it helps, I can try to turn the code that gave me this error into a minimal example and post it to the list.)

Thanks.

-Jason

[Coq-Club] Explanation of setoid_rewrite "Error: build_signature: no constraint can apply on a dependent argument", Jason Gross, 12/24/2012