The Coq mailing list

[mulhern <mulhern AT gmail.com>]

Hi!

Using the refine tactic and I got this error.

User error: execute: found a non-instanciated goal

Aren't non-instantiated goals exactly the things refine is supposed to allow?

I tried giving the placeholders their correct types but got the same
error message.

I then filled in the placeholders with their correct values; luckily
for these particular placeholders the correct value was easy.

Does anybody have any suggestions as to what would cause refine to
give this particular error?

Thanks!

-mulhern

Here is the context of the offending underscores:

(f_equal
                          (fun e : term => match e with
                                           | TmTrue => _
                                           | TmFalse => _
                                           | TmIf _ t _ => t
                                           end) H3 )

H3 has type TmIf t1 t2 t3 = TmIf tm1 tm2 tm3.
So the anonymous function above needs to have the underscores replaced
with subterms of (TmIf t1 t2 t3) thus:

(f_equal
                          (fun e : term => match e with
                                           | TmTrue => t2
                                           | TmFalse => t2
                                           | TmIf _ t _ => t
                                           end) H3)