Rodolphe Lepigre

> The main problem is to turn this set of equations into a confluent and terminating rewrite systems using completion. To this end, you should export this set of equations...

For the record, I implemented the translation to the TRS format based on what was done in Dedukti, hence using the same translation conventions. It would indeed be great if...

Note that this is going to be very tricky, and it is not even clear what the type of a pattern variable is. Or is it? What about constraints for...

Is it really the `bind_mvar` that never returns? Or is it the `unbox`? I'm a bit sceptical that the problem comes from Bindlib: I think it is more likely that...

> @rlepigre In term.ml, you mentioned in a comment that _Meta_full is harmful for efficiency and the last rule of ram_out.lp contains many metavariables. Could this be an explanation? Or...

> I did try to minimize it, but for some reason I couldn't reproduce the explosion on small terms. Maybe I'll give it another go next week. That's be great!...

I really don't think that we should "fix" this, because syntax coloring would then become quite hard. Reserving keywords is really the good way to go I think.

Yes, there is a distinction in other languages: modules cannot usually start with a lowercase letter (e.g., in OCaml). However, in our case that would make the possibility of qualification...

And there is a reason: the one I gave above. Which is in fact a very important reason, and you should agree since you known that having a good editor...

Well, not when you do `require ... as M`. Here, `M` could then be a keyword, and it is standalone.