Fix finite map notations for Coq < 8.13

As discussed, this fixes the notations introduced by !236 (merged) by using parentheses for resolving the notations instead of $. I also added a TODO comment to change it back when support for Coq 8.12 is dropped.

I have tested against Coq 8.13 and Coq 8.12.1 this time around.

Updated script for generating it:

#!/bin/python3

n = 13
# indent by two spaces
indent = "  "


def generate(n):
  # Header
  out = "Notation \"{[ " 

  # notation itself
  for i in range(1, n+1):
    if i > 1:
      out += " ; "
    out += "k" + str(i) + " := a" + str(i)
  out += " ]}\" := \n" 

  # translation of notation
  line = indent + "("
  for i in range(1, n):
    if i > 1:
      line += " ( "
    if len(line) > 70:
      out += line + "\n"
      line = indent + indent 
    line += "<[ k" + str(i) + " := a" + str(i) + " ]>"
  # singleton element
  line += "{[ k" + str(n) + " := a" + str(n) + " ]}"
  for i in range(1, n):
    line += ")" 
  out += line + "\n"

  out += indent + "(at level 1, format\n"

  # format printing
  line = indent + "\"{[ '[hv' "
  for i in range(1, n+1):
    if i > 1:
      # extra space for printing
      line += " ; ']'  '/' "
    # if len(line) > 70:
      # out += line + "\"\n"
      # line = indent + indent + "\""
    line += "'[' k" + str(i) + "  :=  a" + str(i)
  line += " ']' ']' ]}\")"
  out += line

  out += " : stdpp_scope."
  return out

for i in range(2, n+1):
  print(generate(i))