X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=919f71451f63b99884f7037c2a14e240abb92126;hb=68b4f2490c12139c03760b39895619e63b0f38c9;hp=a3a6cb8ed01d44b51dcc91da537809878acbf544;hpb=cffe307107c93392c8663ec246049c0e55d1ed69;p=helm.git
diff --git a/matita/matita/help/C/sec_commands.xml b/matita/matita/help/C/sec_commands.xml
index a3a6cb8ed..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.
@@ -469,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
+
+