From: Luca Padovani <luca.padovani@unito.it>
Date: Fri, 30 May 2003 16:38:16 +0000 (+0000)
Subject: * inner types file generation ported to V7_3_new_exportation
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=95e3f864d28d8577da100f1a775d4cd0a38d8882;p=helm.git

* inner types file generation ported to V7_3_new_exportation
---

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index f498effb6..df460edce 100644
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -411,10 +411,11 @@ let
          (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
            [< x ;
               X.xml_nempty "TYPE" ["of",id]
-               [< print_term ids_to_inner_sorts synty ;
-                  match expty with
-                     None -> [<>]
-                   | Some expty' -> print_term ids_to_inner_sorts expty'
+               [< X.xml_nempty "synthesized" []
+	         [< print_term ids_to_inner_sorts synty >] ;
+                 match expty with
+                   None -> [<>]
+                 | Some expty' -> X.xml_nempty "expected" [] [< print_term ids_to_inner_sorts expty' >]
                >]
            >]
          ) ids_to_inner_types [<>]