The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  I'm trying to figure out how to write the following Ltac:

match goal with:

  | |- context[ let ?lhs := ?rhs in _ ] => ?????

end

now, if "lhs" is something like (a::b) or (x,y) or (Constructor t u z) I would like to "destruct rhs"

if "lhs" is a single varaible, I don't want to "destruct rhs"

Is there a way to phrase this, to basically say "lhs is not a single var"?

Thanks!