Ssreflect Users Discussion List

[<>]

Hello.

Almost always I use <apply:> instead of <apply> to benefit from ssr's  
matching algorithm. But a few of times I have got an error message
"Could not fill dependent hole in "apply""
and I had to switch to <apply>.  

Can I ask why <apply:> does not subsume <apply>, 
which sounds handy. 

Besides, I have a feature wish:
it would be nicer if I get a better error message than 
"Cannot apply lemma" for <apply: h x> where "h x" does not type
check. I.e. I want to see the type error message. 
As a result my al strategy tends to use <apply> first to eliminate
type errors, then switch to <apply:> to eliminate "cannot infer a term
for this placeholder".

Best regards
Keiko