From 48aa99d1d9659e55d68ab3ef50b10bc6165eee03 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 29 Jun 2006 10:53:30 +0000 Subject: [PATCH] Documentation for variant fixed (the type and body are NOT optional). --- helm/software/matita/help/C/sec_terms.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index 30692211e..d521ac870 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -479,7 +479,7 @@ Notice that the command is equivalent to definition f: T ≝ t. - <emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;] + <emphasis role="bold">variant</emphasis> &id;<emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> &term; variant variant f: T ≝ t Same as theorem f: T ≝ t, but it does not -- 2.39.2