Provide a reinit data for Ltac2 notations with entry level 4.

The grammar engine has the great idea to silently delete empty levels on rule
removal. Since Ltac2 level 4 is initially empty, it means that when backtracking
on the loading of the Ltac2 plugin, the grammar would be in a state where the
level 4 was not there at all.

There is a dedicated API for that situation in Pcoq, but it is kind of crazy
that we have to use this kind of workaround when the problem is clearly that
gramlib has the wrong default.

Fixes #14156: Ltac2 broken with async.

0 files changed, 0 insertions, 0 deletions