]> matita.cs.unibo.it Git - helm.git/commitdiff
match x in IDENT and not TERM
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 10 Apr 2007 14:28:33 +0000 (14:28 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 10 Apr 2007 14:28:33 +0000 (14:28 +0000)
matita/help/C/sec_terms.xml

index bd2d8c9c9cdb8a5331487f08b8039f6e8d719589..05385f666b3a41ad4267a1977c0e8c8dac9aa4d5 100644 (file)
       <entry/>
       <entry>|</entry>
         <entry><emphasis role="bold">match</emphasis> &term; 
-        [ <emphasis role="bold">in</emphasis> &term; ]
+        [ <emphasis role="bold">in</emphasis> &id; ]
         [ <emphasis role="bold">return</emphasis> &term; ]
         <emphasis role="bold">with</emphasis>
       </entry>