switch off profilers

[helm.git] / helm / software / matita / help / C / sec_tactics.xml

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index bdfb3e5db83f5a4d9dc98bc7c7a880f89130684a..7647232613daff64928d14d507f7d120439f736e 100644 (file)
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -597,13 +597,13 @@
   <sect1 id="tac_demodulate">
     <title>demodulate</title>
     <titleabbrev>demodulate</titleabbrev>
-    <para><userinput>demodulate</userinput></para>
+    <para><userinput>demodulate auto_params</userinput></para>
     <para>
       <variablelist>
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">demodulate</emphasis></para>
+            <para><emphasis role="bold">demodulate</emphasis> &autoparams;</para>
           </listitem>
         </varlistentry>
         <varlistentry>