Hola.
No tengo claro si cambió algo en la última versión de Coq pero en cada sección que lo uses entiendo que podés poner algo como:
Infix "simbolo" := cons_instr (at level 60, right associativity). (* donde cons_instr es el constructor correspondiente en LInstr *)
Saludos, Carlos