fthire

Is this really a bug? I would say that the error message is not correct instead.

I think that saying `unsatisfiable constraints` here is a real mistake because of the arguments you have made. Instead, it should say that it could not compute a substitution. But...

@Gaspi @GuillaumeGen

@EmilieGrienenberger if your object is "opaque", meaning that it is defined with the `thm` keyword, then its proof should not appear in the `dko`: [see here](https://github.com/Deducteam/Dedukti/blob/8d7ecb09f94138c6202acba549fe842ed9e5b753/api/env.ml#L130). In general, I am...

If my understanding is correct, the current behavior is to export only the statement of `thm_1`, `thm_2`, ... But this behavior is not the one you want. Instead, since `thm_1`,...

@Gaspi @GuillaumeGen

@fblanqui @rlepigre Giving names to rules will be useful to do meta rewriting anyway.

The CIC encoding used for Matita or Coq might need that kind of thing. We are facing with "probably" a blow up which is triggered by a non-linear rule needed...

Well this answer your second question. Since we don't know yet, we have to experiment and for @Gaspi and I, it is far more easier to experiment on a code...

I disagree, it should be accepted! 1. As long as we postponed confluence, termination as meta properties to be checked, the rewrite engine should accept the system. However, we don't...