The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Thanks for your help Eric!

On Tue, Jan 19, 2016 at 9:10 PM, Eric Mullen <emullen AT cs.washington.edu> wrote:

Try making sure that d11 and d10 come into scope before ?1179. Likely what happened is that ?1179 can't unify with whatever you have on the right side, because it has to unify in the context that existed when it was created (not the current context).

I believe that what I've said is true for 8.4, and I think it has changed in 8.5.

Eric

On Tue, Jan 19, 2016 at 3:54 PM Saulo Araujo <saulo2 AT gmail.com> wrote:

Hi,

After using eexists and performing some manipulation, I need to proove a goal of the form

Some ?1179 = Some (coeficient d11 d10)

Which tactic could I use to make Coq understand that there exists a value for ?1179 (i.e. coeficient d11 d10) that makes Some ?1179 = Some (coeficient d11 d10) true?

In other similar situation, reflexivity did the tricky...

I really appreciate any help you can provide,

Saulo Araujo