coq: fix camlp5 --transitional dependency

I think this should fix the problem described in issue #22672 by @mcandre.

The problem was that when `camlp5` was being called, it was not in the path. Creating a `Tab` for `camlp5` and getting the `unused_options` seems much more reliable.

However the fact that `TransitionalMode` is made into an explicit `Requirement` in this way still seems like a hack. I would have removed it but I couldn't figure out a way to specify, using only `depends_on`, that a formula should be built _**without**_ a particular option.

To the experts: is it somehow possible to check this (that `camlp5` is _**not**_ built with `--strict`) using only `depends_on`? If not, it might indicate a need to generalize it so that it works both for specifying options that should be excluded _**and**_ excluded in dependencies.