[ ] 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. (#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] (#386)
CC @CohenCyril @pi8027
HB.instance Definition _ : m (T^d) := ...
looks up canonical structures onT^d
using coq's unification which finds also instances forT
. This should be blocked via a flag. Default value unclear. (#257)HB.sature (_ ^d)
to focus saturation on the given subject#[primitive]
lack proper refolding, since the projection is (in elpi)app[primitive (proj P N),s|args]
rather thanapp[global (const P),s|args]
(#386) CC @CohenCyril @pi8027