Probably `setup_tactic_parser` can be integrated to use `open_locale` instead

[khoek]

[fpvandoorn]

There are two (fixable) issues:

• setup_tactic_parser opens namespaces, which open_locale currently cannot do. This is easily fixed.
• It would require a bunch more tactic files to import tactic.localized (or move the contents of tactic.localized to tactic.core).

I can do this, if you think this is desirable.

[cipher1024]

How big is tactic.localized and how much does it depend on? This is a feature I would really love to have access to everywhere.

setup_tactic_parser opens namespaces, which open_locale currently cannot do. This is easily fixed.

I don't know how I feel about this. On one hand, setup_tactic_parser clearly overlaps with open_locale but on the other hand, what other use case do we have for open_locale opening namespaces?

[fpvandoorn]

It's like 50 lines, excluding the header of the file. It depends on the function emit_code_here, but nothing else.

I could see some use cases for open_locale opening namespaces. For example, open_locale real might define some nice local notations and open the namespace real.

The disadvantage is that open_locale and open are then not orthogonal anymore, which might cause confusion.

[cipher1024]

On the other hand, could we say that open_locale always opens the namespace of the name of the locale? We could add an option to inhibit that behavior but we could understand open_locale as taking notations from a namespace. What do you think?