Thiago Felicissimo

I don't think that we should prefer one solution instead of another, but my point is that I thought that the unification tried to preserve all solutions. If unification is...

> * Why "if R is locally confluent without using beta to close critical pairs and moreover R is SN then R+beta is confluent"? We can conclude confluence of R...

> Adding integers does not allow tracing back symbols and rewrite rules. It should be easy to identify in the output what comes from the input. There is indeed a...

I have now put back qualified names, and removed the afsm export as I don't need it anymore

What this shows is that it is unsound to deduce that `nil A'` and `nil A''` have a common reduct just because `A'` and `A''` are convertible by typing constraints....

``` constant symbol N : TYPE; constant symbol 0 : N; constant symbol P : N → TYPE; constant symbol p0 : P 0; symbol c (x : N) :...

I see, thanks for the `debug +s;` tip, it's already quite helpful. But are you planning on re-adding names in the future? I think it would be much better for...