Dear community,
I would like to know if there is a native Ltac2 version of the timeout
from Ltac1.
I have tried to use this tactic in Ltac2, but I get the Unbound value timeout
error. For instance, the following example works:
Ltac timed_auto := timeout 60 (first [solve [auto] ] ).
but the following does not
Ltac2 timed_auto () := timeout 60 (first [solve [auto] ] ).
I have not found anything about this on the Ltac2 Wiki, and also not in the LTac2 Std library.