Syntax error in generated code (need to avoid ocaml keywords)

SkySkimmer / coq-ltac2-compiler

GNU Lesser General Public License v2.1

5 stars 0 forks source link

Syntax error in generated code (need to avoid ocaml keywords) #4

Closed Janno closed 1 year ago

Janno commented 1 year ago

File "/tmp/tac2compile_6802a9/f6fbe42.ml", line 5843, characters 47-52:
5843 |       ((make_app1_kn102_f__ preWait p) >>= fun class ->
                                                      ^^^^^
Error: Syntax error

The corresponding Ltac2 code is:

    let class := make_app1 preWait p in

I think class is restricted keyword: https://v2.ocaml.org/releases/4.07/htmlman/manual049.html