The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Hi,

Given this goal:

 T:Type
 ...
 ===============
 Prop

I try to do
 refine (forall t:T, foo bar _ baz qux)

But then I get:

 User error: Refine: proof term contains metas in a product

I'd like to understand why it is an error to have holes in a
product. What's wrong with that? Shouldn't I get something like the
goal

 T:Type
 ...
 t:T
 ===============
 (inferred type of hole)

So, for example, if foo:forall n:nat, n>0 -> A -> B -> Prop

the conclusion of the goal I would expect to get is:

 bar > 0

What am I missing?


Thanks in advance,

-- 
Lionel