Gabriel Hondet

No it isn't. It contains the `redopaque` mechanism, and I use it to type check PVS files, but it should not be merged anyway.

Ah it must be because I wasn't looking at master, sorry

> Right, we could add some error message before assert false saying that some lpo file is maybe out of date, but we should keep the assert false, don't you...

It can since sedlex handles utf16: https://ocaml-community.github.io/sedlex/sedlex/Sedlexing/Utf16/index.html

All right, with the new parser, hopefully it's just a switch in the lexer (using the utf16 module instead of utf8).

It comes from the LSP server, if we have a look in the logs, ``` $ tail lambdapi_lsp_log.txt "textDocument": { "uri": "file:///tmp/%CE%B7/f.lp" }, "position": { "line": 0, "character": 5 }...

Just a side note, on developing shell scripts, I couldn't recommend enough [ShellCheck](https://www.shellcheck.net/) (can be installed and used by flycheck).

Perhaps, because of the comments, we must not allow `/` in identifiers.

It seems to me that the following does what we want https://gist.github.com/gabrielhdt/e687e60f2eb14c14282e310f556e2230 it allows `$`, `?` but still parses `$foo` as a pattern, it forbids `/` and allows `*`.

The pull request #818 solves the issue