Procedural: the statement body and it inner types must satisfy the Barendregt

[helm.git] / components / cic_acic / cic2Xml.ml

diff --git a/components/cic_acic/cic2Xml.ml b/components/cic_acic/cic2Xml.ml
index 7e97dea6fb0b5fef93d430632c901f8e043688b7..c90bc348c662c5c35dcdf3951946ee4de06ea53e 100644 (file)
--- a/components/cic_acic/cic2Xml.ml
+++ b/components/cic_acic/cic2Xml.ml
@@ -269,7 +269,8 @@ let print_term ?ids_to_inner_sorts =
 
 let xml_of_attrs attributes =
   let class_of = function
-    | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
+    | `Coercion n -> 
+        Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n]
     | `Elim s ->
         Xml.xml_nempty "class" [None,"value","elim"]
          [< Xml.xml_empty
@@ -279,20 +280,28 @@ let xml_of_attrs attributes =
     | `Record field_names ->
         Xml.xml_nempty "class" [None,"value","record"]
          (List.fold_right
-           (fun (name,coercion) res ->
+           (fun (name,coercion,arity) res ->
              [< Xml.xml_empty "field" 
-                [None,"name",if coercion then name ^ " coercion" else name]; 
+                [None,"name",
+                  if coercion then 
+                    name ^ " coercion " ^ string_of_int arity 
+                  else 
+                    name]; 
               res >]
            ) field_names [<>])
     | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
+    | `InversionPrinciple -> Xml.xml_empty "class" [None,"value","inversion"]
   in
   let flavour_of = function
     | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
+    | `MutualDefinition ->
+        Xml.xml_empty "flavour" [None, "value", "mutual_definition"]
     | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"]
     | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"]
     | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
     | `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"]
     | `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"]
+    | `Axiom -> Xml.xml_empty "flavour" [None, "value", "axiom"]
   in
   let xml_attr_of = function
     | `Generated -> Xml.xml_empty "generated" []