coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] gprogress tactical?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] gprogress tactical?
Date: Fri, 23 Jan 2015 23:43:19 -0800

Hi,

In trunk/8.5, is there a tactical that means "progresses in at least one goal"? I tried `progress [> intros ]`, but this fails if any of the goals has no hypotheses to introduce, and I want it to fail only if all of the goals have no hypotheses to introduce.

Thanks,

Jason

[Coq-Club] gprogress tactical?, Jason Gross, 01/24/2015
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/24/2015
  - Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/24/2015
    - Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/24/2015
      - Re: [Coq-Club] gprogress tactical?, Pierre-Marie Pédrot, 01/25/2015
        
        Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/25/2015
      - Re: [Coq-Club] gprogress tactical?, Jason Gross, 01/25/2015
        
        Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/25/2015
        
        Re: [Coq-Club] gprogress tactical?, Arnaud Spiwack, 01/26/2015
        
        Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/26/2015
        Re: [Coq-Club] gprogress tactical?, Arnaud Spiwack, 01/26/2015