The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The associated error message (from Set Ltac Debug) is "Only bound indices allowed in second order pattern matching."  I'm not quite sure if this is expected behavior.  However, there's definitely a bug here, in that "idtac f" mentions x(!), which is bound inside the function, but not at top level.  (Set Ltac Debug gives me "Ltac variable f depends on pattern variable name x which is not bound in current context.")

I've submitted a bug for both of these at https://coq.inria.fr/bugs/show_bug.cgi?id=3130.

-Jason

On Tuesday, September 17, 2013, Adam Chlipala wrote:

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