Currently, when translating a constant c, every other constant mentioned in the body of c must have been already translated. Just like paramcoq, the implementation should compute the dependencies and automatically translate them in the right (topological) order.
Currently, when translating a constant
c, every other constant mentioned in the body ofcmust have been already translated. Just like paramcoq, the implementation should compute the dependencies and automatically translate them in the right (topological) order.