Remove the deprecated clear modifier.

[ppedrot]

It has been deprecated since 8.17, long enough for people to have realized this.

[ppedrot]

I will write a cleanup following this removal, but I prefer having this PR separate.

[herbelin]

I may have missed a discussion, but what are the objections against a clear modifier? It seems to me to be a useful feature.

[ppedrot]

@herbelin see #16407

[herbelin]

The discussion was more about the syntactic and semantics difference between ssr and vanilla for the clear feature, not about the principle of such feature. I feel uncomfortable to take such kind of decision of removal of an a-priori useful feature without a prior vision of where we are going in general regarding tactics. Also, I'd like to remind that if I did not document and advertise the clear flag further, and did not fully develop it, it was precisely in the hope of a discussion about what is our vision about tactics (especially after the trauma that the implementation of the % intropattern created).

My perception is that we are postponing for many years the question of what is our model regarding tactics. I'm unsure we can afford continuing postponing it. I hope the discussion on the long-term roadmap will help us communicating between us.

[jfehrle]

Suggested change

	the clear modifier which was deprecated since 8.17
	the :n:`clear` modifier which has been deprecated since 8.17

[ppedrot]

Despite having a similar behaviour, this is not the clear tactic, so I'm not sure we want to do this. The previous changelog entry did not have a special rendering for this word (see #16407).

[herbelin]

PS: My previous remarks applied to the code of the clear modifier. Deactivating the parsing rule is consistent with #16407.

[ppedrot]

@herbelin so there is no problem with this PR per se then?

[SkySkimmer]

@coqbot merge now