Control in the trocq tactic

[ecranceMERCE]

It would be interesting to have additional arguments in the trocq tactic to provide guidance and tell Trocq which terms must change, and which must not. It would for example allow for several parametricity relations to coexist and the user to choose which one is used for each occurrence of the term to translate.

For instance:

nat ~ bin_nat :. nat_binR
nat ~ nat :. natR

In the first goal below, the first instance would be used for n, but in the second goal, if bitvector ~ bitvector, then the second instance would be used for n.

forall (n : nat), n = n

forall (n : nat) (v : bitvector n), v = v

[CohenCyril]

Notice that bitvector is not parametric on nat but imposes nat ~ nat :. natR, if we make sure trocq is guided by typeconstraint first and user input second, then we get the good behaviour.