Dedukti
Dedukti copied to clipboard
Fix #295
This is the simplest fix to #295 . Consequence of this fix is that now, if one names a module with a keyword, they have to require it using "{|...|}". This seems to be a very sensible constraint to me, but it is a non-backward compatible change.
There is another possibility, to avoid this change, which is to duplicate the system we created for ident
with the sident
and buffering but for mident
, so to have a smident
so to say.
If backward compatibility is crucial (ie more important than avoiding code duplication for maintainability), then I can implement the other proposed solution, it is quite simple too.