The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

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