Translation: use notations for the new monadic operators

Use more monadic notations in the Coq translation, especially for the new monadic notations used in the protocol with snippets like:

let open Result_syntax in
let* () = check_gas_limit ~hard_gas_limit_per_operation ~gas_limit in
let gas_limit_fp = Arith.fp gas_limit in
let* () =
  error_unless
    Arith.(gas_limit_fp <= remaining_block_gas)
    Block_quota_exceeded
in
return (Arith.sub remaining_block_gas gas_limit_fp)

being translated to:

    let? '_ := check_gas_limit hard_gas_limit_per_operation gas_limit in
    let gas_limit_fp := Arith.fp_value gas_limit in
    let? '_ :=
      Error_monad.error_unless (Arith.op_lteq gas_limit_fp remaining_block_gas)
        (Build_extensible "Block_quota_exceeded" unit tt) in
    return? (Arith.sub remaining_block_gas gas_limit_fp).

instead of:

    Error_monad.Result_syntax.op_letstar
      (check_gas_limit hard_gas_limit_per_operation gas_limit)
      (fun function_parameter =>
        let '_ := function_parameter in
        let gas_limit_fp := Arith.fp_value gas_limit in
        Error_monad.Result_syntax.op_letstar
          (Error_monad.error_unless
            (Arith.op_lteq gas_limit_fp remaining_block_gas)
            (Build_extensible "Block_quota_exceeded" unit tt))
          (fun function_parameter =>
            let '_ := function_parameter in
            Error_monad.Result_syntax._return
              (Arith.sub remaining_block_gas gas_limit_fp))).