Decl_mode
Decl_interp
Decl_proof_instr
Ppdecl_proof
G_decl_mode