The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

A small self-contained example would definitely help.

When rewrite fails, I often find it useful to directly invoke or apply eq_rect or eq_ind (these are automatically generated induction principles for the equality type).

If even that fails, I ask someone to help me with writing a dependent pattern match on the proof of equality (e.g. E1 in your case).

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Fri, May 8, 2015 at 8:38 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

If there is any additional information I can provide to help to figure out what is causing this?
Some proofs which were working in 8.4 does not work in 8.5 because of this error and I do not
see anything wrong here. I suspect it might be a bug in 8.5 branch.

Vadim

> On May 7, 2015, at 12:43 , Vadim Zaliva <vzaliva AT cmu.edu> wrote:
>
> 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
>

Sincerely,
Vadim Zaliva

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