Merge branch 'ralf/ascii' into 'master'

mention that the ASCII syntax exists (but we recommend unicode)

See merge request !470
4 jobs for master in 12 minutes and 18 seconds (queued for 5 seconds)
Status Job ID Name Coverage
  Build
canceled #79768
fp
build-coq.8.10.2

00:05:00

canceled #79767
fp-timing
build-coq.8.11.2

canceled #79766
fp
build-coq.8.12.dev

00:12:18

canceled #79769
fp
build-coq.8.9.1

00:02:48