Change in the Constructor tactic?

Using Coq
1

Recently I was porting some Coq code from an older version of Coq to the latest version.
In particular, I was trying to get
https://github.com/Formal-Systems-Laboratory/coinduction to build.

I ran across some proofs which had steps of the form:

constructor(tactic)

or

econstructor(tactic)

where “tactic” was some tactic.

For example, in the coinductive-proofs/common/proof.v file, we find this:

Lemma reaches_stable :
(forall x P, reaches x P -> step reaches x P).
Proof. destruct 1;econstructor(eassumption). Qed.

Apparently some prior version of Coq accepted this form, but the new version does not. It seemed that the intent was that when constructor tried to use “constructor 1, then constructor 2, etc”,
that it would reject a constructor unless following it with the tactic would succeed. This is
useful in cases where more than one of the constructors match the current goal. So it
only chooses the one that succeeds.

This seems like a useful feature. To work around the lack of this feature I ended up
using some Ltac like this:

Ltac myconstructor tac :=
tryif constructor 1; tac then idtac else
tryif constructor 2; tac then idtac else
tryif constructor 3; tac then idtac else
tryif constructor 4; tac then idtac else
tryif constructor 5; tac then idtac else
tryif constructor 6; tac then idtac else
tryif constructor 7; tac then idtac else
fail.

But that seems kind of kludgy.
I’ve not been able to find a record of this construct being allowed in previous Coq versions and was wondering if anyone is familiar with the feature, if it in fact existed, and if so, why was it removed as it seems like a userful feature.

Rich

2

In changes for 8.5 you can see

  * Tactic "constructor" is now fully backtracking. In case of
    incompatibilities (e.g. combinatoric explosion), the former
    behavior of "constructor" can be retrieved by using instead
    "[> once constructor ..]". Thanks to backtracking, undocumented
    "constructor <tac>" syntax is now equivalent to
    "[> once (constructor; tac) ..]".

So for instance

Inductive bla := C (_:nat) | D.

Lemma foo : bla.
Proof. [> once (constructor; assumption)]. Defined.
Print foo. (* foo = D *)