The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Great, your black magic work-around seems to work like a charm! Thanks a lot!

2015-01-30 15:54 GMT-05:00 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
>
>



-- 
Arthur Azevedo de Amorim