coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Ways to match in the goal by type?
Date: Sun, 20 Mar 2016 00:52:30 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f172.google.com
Ironport-phdr: 9a23:cp0hxBRs9EZ1S3CbIKHciACWWNpsv+yvbD5Q0YIujvd0So/mwa64YB2N2/xhgRfzUJnB7Loc0qyN4/CmATxLu83Q+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq82VO1UD3mHsKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7oW/vh7aCACL+3E0U2MMkxMODRKTvz/gWZKkkCLhsew19zOdJta+GbI9QjOk4L1sUwS5oCgCPj89tmrQj5oj3+pgvBu9qkknkMbva4aPOa8mcw==

Hi,

I just ran into a tactic that's 20x slower in 8.4 than in 8.4. Basically the tactic is:

match goal with

| [ |- appcontext[?e] ]

=> not is_var e;

not is_evar e;

match type of e with

| _ <= _ => idtac

end;

generalize e

end

where not is a tactical of my own devising that does the obvious thing.

Is there a better way to do this? One that doesn't require doing stuff with every single subterm of the goal type?

Thanks,

Jason

[Coq-Club] Ways to match in the goal by type?, Jason Gross, 03/20/2016
- Re: [Coq-Club] Ways to match in the goal by type?, Jonathan Leivent, 03/20/2016