X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fhelp%2FC%2Fcommand_include.html;fp=matita%2Fmatita%2Fhelp%2FC%2Fcommand_include.html;h=0000000000000000000000000000000000000000;hb=9d5a0d55e331b348d44b6d50d3d67e62b60a0e18;hp=52eb85bb67baa0dd809f58e2a417344d83c6f740;hpb=7b6ca76a0ed511b288b654729c9758277dbcd352;p=helm.git diff --git a/matita/matita/help/C/command_include.html b/matita/matita/help/C/command_include.html deleted file mode 100644 index 52eb85bb6..000000000 --- a/matita/matita/help/C/command_include.html +++ /dev/null @@ -1,17 +0,0 @@ - -include
include
Prev Chapter 9. Other commands Next

include

include "s"

-

Synopsis:

include qstring

Action:

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. -

-

Prev Up Next
coercion Home include alias
\ No newline at end of file