Reviewed-by: ppedrot

`Global.lookup_constant` fails with an assertion instead of `Not_found`. Some
code relied upon `Not_found`.

Reviewed-by: mattam82

The old code was generating different patterns, depending on whether
a projection with parameters was expanded or not. In the first case,
parameters were present, whereas in the latter they were not.

We fix this by adding dummy parameter arguments on sight.

Fixes #14009: TC search failure with primitive projections.

As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.

It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.

We thus remove all bitrotten dead code.

Reviewed-by: ppedrot

As a bonus ltac2 can produce bullet suggestions.

This is more consistent with other code.