Gaspard Férey

It's a bit of a bug that the error message is incorrect, isn't it ? It could also turn into a "real" bug as "unsatisfiable constraints" essentially means "this rule...

This issue arose when discussing with Gabriel about reduction strategy. - In (old) Dedukti, rules are always used in the order of declaration which is a useful guarantee when one...

> But could you please first motivate this extension: in which application do you need this? Second, why do you open an issue in Dedukti and not in Lambdapi? -...

Great, I'm looking forward to it, thanks! As long as it's not too much work to implement I agree that declaring S-injectivity (even unchecked) is the best way to do...