Closed ppedrot closed 4 months ago
This confuses my text editor and I think this is actually useless. Indeed, looking at the code of Elpi seems to indicate that we do not need one additional level of escaping there.
@gares please check that this analysis is correct.
This confuses my text editor and I think this is actually useless. Indeed, looking at the code of Elpi seems to indicate that we do not need one additional level of escaping there.
@gares please check that this analysis is correct.