' not allowed at the beginning of an identifier

[fblanqui]

Dedukti/parsing/lexer.mll

Line 25 in 3dbbffd

let ident = ['a'-'z' 'A'-'Z' '0'-'9' '_' '!' '?']['a'-'z' 'A'-'Z' '0'-'9' '_' '!' '?' '\'' ]*

it may be useful to write 'a like in ML and systems based on ML (Isabelle, HOL-Light, HOL4)

[GuillaumeGen]

It clearly is possible and easy (you pointed the line to change).
Hence the question is do we want to do it.

Benefits : 'a becomes a valid identifier, allowing us to have code closer to Ocaml naming convention.
Drawbacks : we lose the ability to have a native type of characters with the 'a' syntax.

Since I see the point for translation to have a more idiomatic syntax and I hardly see someone adding a native type of characters in Dedukti, I am in favor of this change.