coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] coq8.5: "no constraint can apply on a dependent argument"

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] coq8.5: "no constraint can apply on a dependent argument"
Date: Thu, 7 May 2015 12:43:36 -0700

I am trying to port some of my proofs from 8.4 to 8.5 (I am using latest
snapshot
from git) and getting error message I have not encountered before:

E1 : xa = ya
E2 : xb = yb
============================
(Vtail xa, Vtail xb) = (Vtail ya, Vtail yb)

rewrite E1, E2.

Error: build_signature: no constraint can apply on a dependent argument

What does it mean?

Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva

[Coq-Club] coq8.5: "no constraint can apply on a dependent argument", Vadim Zaliva, 05/07/2015
- Re: [Coq-Club] coq8.5: "no constraint can apply on a dependent argument", Vadim Zaliva, 05/09/2015
  - Re: [Coq-Club] coq8.5: "no constraint can apply on a dependent argument", Abhishek Anand, 05/09/2015
    - Re: [Coq-Club] coq8.5: "no constraint can apply on a dependent argument", Vadim Zaliva, 05/10/2015
      - Re: [Coq-Club] coq8.5: "no constraint can apply on a dependent argument", Abhishek Anand, 05/10/2015
        
        Re: [Coq-Club] coq8.5: "no constraint can apply on a dependent argument", Vadim Zaliva, 05/10/2015