The Coq mailing list

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

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
Inductive foo : Type :=
| Foo0
| Foo1
| Foo2
| Foo3
| Foo4
| Foo5
| Foo6
| Foo7
| Foo8
| Foo9.

Inductive bar (f : foo) : Prop :=
| Bar0 : f = Foo0 -> bar f
| Bar1 : f = Foo1 -> bar f
| Bar2 : f = Foo2 -> bar f
| Bar3 : f = Foo3 -> bar f
| Bar4 : f = Foo4 -> bar f
| Bar5 : f = Foo5 -> bar f
| Bar6 : f = Foo6 -> bar f
| Bar7 : f = Foo7 -> bar f
| Bar8 : f = Foo8 -> bar f
| Bar9 : f = Foo9 -> bar f.

(* Takes forever *)
(*
Goal forall f, bar f.
intros f.
destruct f; once (constructor; reflexivity).
Qed.*)

(* Works instantly. *)
Goal forall f, bar f.
intros f.
destruct f.
constructor; reflexivity.
constructor; reflexivity.
constructor; reflexivity.
constructor; reflexivity.
constructor; reflexivity.
constructor; reflexivity.
constructor; reflexivity.
constructor; reflexivity.
constructor; reflexivity.
constructor; reflexivity.
Qed.