X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=7e22f33043d39ec5e0fcb62e7ce0c20ca1e41593;hb=e91eb82d2b5e032907758bff0b474d62d57463dc;hp=4d788f39aa3feb8ed01961dd48a782b9ec2a6436;hpb=ca41435a6021292ccba239aa173651c0be705b45;p=helm.git
diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml
index 4d788f39a..7e22f3304 100644
--- a/helm/software/matita/help/C/sec_commands.xml
+++ b/helm/software/matita/help/C/sec_commands.xml
@@ -74,6 +74,57 @@
+
+ eval
+ eval red on t
+
+
+
+ Synopsis:
+
+ eval
+ &reduction-kind;
+ on
+ &term;
+
+
+
+ Action:
+
+ Opens a CIC browser window that shows
+ the reduct of
+ t
+ together with its type.
+
+
+
+
+
+
+ prefer coercion
+ prefer coercion u
+
+
+
+ Synopsis:
+
+
+ prefer coercion
+ (&uri; | &term;)
+
+
+
+
+ Action:
+
+ The already declared coercion u
+ is preferred to other coercions with the same source and target.
+
+
+
+
+
+ coercioncoercion u with ariety saturation nocomposites
@@ -328,7 +379,7 @@
qed
-
+ qed
@@ -350,5 +401,188 @@
-
+
+
+ inline
+ inline "s" params
+
+
+
+ Synopsis:
+
+
+ inline &qstring; &inlineparams;
+
+
+
+
+ Action:
+
+ Inlines a representation of the item s,
+which can be the URI of a HELM object. If an entire HELM directory (i.e. a base
+URI) or the path of a *.ma source file is provided, all the contained objects
+are represented in a row.
+If the inlined object has a proof, this proof is represented in several ways
+depending on the provided parameters.
+
+
+
+
+
+
+ inline-params
+