From cffe307107c93392c8663ec246049c0e55d1ed69 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 18 Nov 2011 15:39:39 +0000 Subject: [PATCH] ... --- matita/matita/help/C/sec_commands.xml | 32 +++++++++++++++++++++++++-- matita/matita/help/C/sec_tactics.xml | 2 +- 2 files changed, 31 insertions(+), 3 deletions(-) diff --git a/matita/matita/help/C/sec_commands.xml b/matita/matita/help/C/sec_commands.xml index 3deaf4b51..a3a6cb8ed 100644 --- a/matita/matita/help/C/sec_commands.xml +++ b/matita/matita/help/C/sec_commands.xml @@ -326,8 +326,36 @@ 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. + 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. + + + + + + + + include alias + include alias "s" + + + + Synopsis: + + include alias &qstring; + + + + Action: + + Every + interpretation + declared in the file s is re-declared + so to make it the preferred choice for disambiguation. diff --git a/matita/matita/help/C/sec_tactics.xml b/matita/matita/help/C/sec_tactics.xml index 4687868ad..2ac2cfc65 100644 --- a/matita/matita/help/C/sec_tactics.xml +++ b/matita/matita/help/C/sec_tactics.xml @@ -167,7 +167,7 @@ - + ## ## ## -- 2.39.2