The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

It is not forever.  Just approximately 2 * 10^(number of goals - 4) s.  On 10 goals, you should expect to wait about 2 * 10^10 seconds, or over 600 years.

I've reported this as bug 3969.

Here is a black magic work-around (I'll post a description of how I'm guessing this works to the bug tracker):

  repeat ([ > once (constructor; reflexivity) | .. ])

If you want, you could even do:

Tactic Notation "constructor" tactic3(tac) := repeat ([ > once (constructor; tac) | .. ]).

and then [constructor (reflexivity)] does what it used to.

On Fri, Jan 30, 2015 at 3:31 PM, Arthur Azevedo de Amorim <arthur.aa AT gmail.com> wrote:

Dear Club,

The CHANGES file for 8.5beta1 states that the old "constructor tac"
idiom has been superseeded by "once (constructor; tac)", but I haven't
been able to get it to work: right now, putting "once (constructor;
tac)" causes the script to run seemingly forever, *even though copying
and pasting that line multiple times makes it solve the goal
instantly*.

I've attached a simplified test case illustrating the behavior.

Any ideas on what causes this or how to get it fixed?

Thanks!

--
Arthur Azevedo de Amorim