include qstring

Every coercion, notation and interpretation that was active when the file s was compiled last time is made active. The same happens for declarations of disambiguation hints (aliases). On the contrary, theorem and definitions declared in a file can be immediately used without including it.

The file s is automatically compiled if it is not compiled yet.

If the file s was already included, either directly or recursively, the commands does nothing.