The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 09/15/2013 06:01 PM, robert wrote:

However, I'm still sort of stuck; trying to apply the technique to my setting gives me odd behavior I don't undersdand. In the final goal below, I expect the match to go into the "app" branch, but instead it goes into the "app no @?" branch. This seems like it might be a bug, because the branch succeeds on my example if I change the pattern to:

 

(plus (@?f x) (@?g x))

 

So maybe it doesn't want to match on partial applications for some reason? Any advice?

That is definitely peculiar.  It may be related to longstanding efforts (e.g., adding [appcontext]) to remove Ltac behavior that unreasonably reveals the representation of function application as n-ary in the kernel.  I'd say it would be reasonable to file a bug report on this one!

Ltac do_sk t k :=(*...*)

 

| (fun (x:?T) => (@?f x) (@?g x)) =>

idtac "app" f g; k 2

 

| (fun (x:?T) => ?f ?g) =>

idtac "app, no @?" f g; k 22