Frédéric Blanqui

This PR provides a new parser for lp files not based on Menhir but written by hand. It is more efficient, provides better error messages and is easier to change...

https://github.com/Deducteam/lambdapi/blob/e119c8cee3647e1d17fa6fdaf1bb6129f42927bc/lambdapi.opam#L82

``` require open Stdlib.Set Stdlib.Prop Stdlib.Nat Stdlib.List; symbol sample_1 (n:ℕ) : π ⊤ ≔ begin induction { } // cursor here end; ``` *Goals* buffer: "No goals", while it should...

``` require open Stdlib.Set Stdlib.Prop Stdlib.Nat Stdlib.List; symbol A:TYPE; inductive V:ℕ → TYPE ≔ Vnil:V 0 | Vcons (x:A) n (v:V n):V(n +1); symbol sample_2 n (v : V n)...

' not allowed at the beginning of an identifier

1

https://github.com/Deducteam/Dedukti/blob/3dbbffdb5c8af3be15bb2c7a59ba263505c3a360/parsing/lexer.mll#L25 it may be useful to write 'a like in ML and systems based on ML (Isabelle, HOL-Light, HOL4)