Frédéric Blanqui

Is this PR still necessary?

Note that the fact that there is currently no `Patt(None,_,_)` is used for computing critical pairs.

43c547dc684135542b8159885514b8219e062844 provides slightly more information.

``` 11:58 ~/src/lambdapi (master) dune exec -- lambdapi check -c tests/OK/why3_quantifiers.lp Loading "/home/blanqui/src/lambdapi/tests/OK/why3_quantifiers.lp" ... Loading "/home/blanqui/src/lambdapi/tests/OK/logic.lp" ... Loading "/home/blanqui/src/lambdapi/tests/OK/bool.lp" ... Loading "/home/blanqui/src/lambdapi/tests/OK/nat.lp" ... Uncaught [Unix.Unix_error(Unix.ECHILD, "waitpid", "")]. ```

There is no problem if we remove the option `-c`. So it must be related to the writing of lpo files.

Currently, in LP: - in the old syntax, variable type declarations are ignored, as it was the case in Dk - in the new syntax, there are no type declaration...

Remark: with the current master version of LP (commit 405c9fe3), I get the same behavior for all these files (and no performance issue): ``` [/home/blanqui/src/lambdapi/ett-in-lambdapi/ETT/failing.lp, 54:0-55:98] Some metavariables could not...

This seems to be a performance problem in Bindlib at the following line in LP (call to bind_mvar): https://github.com/Deducteam/lambdapi/blob/4cdd818a7d4a8b214e5ac904a14e8b959ad0ec0a/src/tool/sr.ml#L151 So I don't know whether it can be fixed quickly...

Ah, my mistake: this is not on master that I have this problem but on a working branch. Sorry.

@rlepigre Wait, I really have a problem with bind_mvar but this is a few lines later, not in a log_enabled section: https://github.com/fblanqui/lambdapi/blob/249b81fadc16b6c24b829d44290422ee57ea161a/src/tool/sr.ml#L171-L175 When running this branch on ram_out.lp with "debug...