X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=919f71451f63b99884f7037c2a14e240abb92126;hb=93db728b3f690d2c683f64833353da685a6f1b65;hp=3deaf4b517ae381d6f1bfe0419f22de521c83278;hpb=8f699ab265e380a2d1ab7dba0ee5e8ba5556a84a;p=helm.git
diff --git a/matita/matita/help/C/sec_commands.xml b/matita/matita/help/C/sec_commands.xml
index 3deaf4b51..919f71451 100644
--- a/matita/matita/help/C/sec_commands.xml
+++ b/matita/matita/help/C/sec_commands.xml
@@ -131,9 +131,7 @@
-->
coercion
- TODO
-
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.
+ 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:
+
+ includealias &qstring;
+
+
+
+ Action:
+
+ Every
+ interpretation
+ declared in the file s is re-declared
+ so to make it the preferred choice for disambiguation.
@@ -441,6 +500,89 @@
+
+ unification hint
+ unification hint n â v1 : T1,⦠vi : Ti; h1 â t1, ⦠hn â tn ⢠tl â¡ tr.
+
+
+
+ Synopsis:
+
+
+ unification hint
+ &nat;
+ â
+ [ &id; [ : &term; ] ,.. ]
+ ;
+ [ &id; â &term; ,.. ]
+ â¢
+ &term; â¡ &term;
+
+
+
+
+ Action:
+
+ Declares the hint at precedence n
+ The file hints_declaration.ma must be
+ included to declare hints with that syntax.
+ Unification hints are described in the paper
+ "Hints in unification" by
+ Asperti, Ricciotti, Sacerdoti and Tassi.
+
+
+
+
+
+
+
+ universe constraint
+ TODO
+
+