warning about loading flexible clauses

[gares]

There is a idiom in Coq-Elpi and HB

do-stuff CL, CL => rest

where CL is a list of clauses.
Typically CL mention unique constants or pi quantified names, eg

pi x y z\ msolve [goal [decl x .., decl y] ...]
msolve [goal CTX _ _ as G|_] :- CTX => solve G

Tracking this pattern statically is not trivial for two reasons:

• some unique data is generated by APIs, eg coq.env.add-const, and not just builtins
• variables loaded via => may be used non linearly, eg CTX => CTX => goal, and in this case functionality is broken

Currently the determinacy analysis raises a warning.

[FissoreD]

This problem is partially solved by using the =!=> operator.