Why "something is LP keyword" is checked during the printing?

[amelieled]

See pretty.ml:

let raw_ident : popt -> string pp = fun pos ppf s ->
  if !check_keywords && LpLexer.is_keyword s then
    fatal pos "%s is a Lambdapi keyword." s
  else Print.pp_uid ppf s

[fblanqui]

pretty.ml is intended to generate valid LP files. It is used to convert Dedukti files to LP files. And Dedukti and LP do not have the same class of identifiers and keywords.

[amelieled]

Ah yes thanks!
Maybe you can move the function is_keyword in pretty.ml because it's only used once in pretty.ml, and not during lexing:

$ rgrep "is_keyword" *
src/parsing/lpLexer.ml:let is_keyword : string -> bool =
src/parsing/pretty.ml:  if !check_keywords && LpLexer.is_keyword s then

[fblanqui]

Done in #759.