issues affecting order.v

[gares]

• HB.instance Definition _ : m (T^d) := ... looks up canonical structures on T^d using coq's unification which finds also instances for T. This should be blocked via a flag. Default value unclear. (Declaring dual bPOrderType and tPOrderType instances fails #257)
• HB.sature (_ ^d) to focus saturation on the given subject
• exported op from a mixing tagged with #[primitive] lack proper refolding, since the projection is (in elpi) app[primitive (proj P N),s|args] rather than app[global (const P),s|args] (#[primitive] HB.mixin breaks the types of constants lifting mixin projections #386)
  CC @CohenCyril @pi8027

[pi8027]

I added pointers to issues dedicated to some items.