X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic%2FcicParser.ml;h=49a5a1ab7cc5d3c48e6a9b9a15a04aca4d0f122f;hb=387c6f39b2e55c887e8947039e5d7f56bce7f7a8;hp=a7ad3c9cf1f88c8cc56cfdadad7c119c3098bc45;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/cic/cicParser.ml b/components/cic/cicParser.ml
index a7ad3c9cf..49a5a1ab7 100644
--- a/components/cic/cicParser.ml
+++ b/components/cic/cicParser.ml
@@ -667,17 +667,25 @@ let end_element ctxt tag =
       push ctxt 
         (match pop_tag_attrs ctxt with
         | [ "value", "definition"] -> Obj_flavour `Definition
+        | [ "value", "mutual_definition"] -> Obj_flavour `MutualDefinition
         | [ "value", "fact"] -> Obj_flavour `Fact
         | [ "value", "lemma"] -> Obj_flavour `Lemma
         | [ "value", "remark"] -> Obj_flavour `Remark
         | [ "value", "theorem"] -> Obj_flavour `Theorem
         | [ "value", "variant"] -> Obj_flavour `Variant
+        | [ "value", "axiom"] -> Obj_flavour `Axiom
         | _ -> attribute_error ())
   | "class" ->
       let class_modifiers = pop_class_modifiers ctxt in
       push ctxt
         (match pop_tag_attrs ctxt with
-        | ["value", "coercion"] -> Obj_class `Coercion
+        | ["value", "coercion"] -> Obj_class (`Coercion 0)
+        | ("value", "coercion")::["arity",n]  
+        | ("arity",n)::["value", "coercion"] -> 
+            let arity = try int_of_string n with Failure _ ->
+              parse_error "\"arity\" must be an integer"
+            in
+            Obj_class (`Coercion arity)
         | ["value", "elim"] ->
             (match class_modifiers with
             | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)
@@ -690,8 +698,15 @@ let end_element ctxt tag =
                 (function
                   | Obj_field name -> 
                       (match Str.split (Str.regexp " ") name with
-                      | [name] -> name, false
-                      | [name;"coercion"] -> name,true
+                      | [name] -> name, false, 0
+                      | [name;"coercion"] -> name,true,0
+                      | [name;"coercion"; n] -> 
+                          let n = 
+                            try int_of_string n 
+                            with Failure _ -> 
+                              parse_error "int expected after \"coercion\""
+                          in
+                          name,true,n
                       | _ -> 
                           parse_error
                             "wrong \"field\"'s name attribute")
@@ -702,7 +717,8 @@ let end_element ctxt tag =
             in
             Obj_class (`Record fields)
         | ["value", "projection"] -> Obj_class `Projection
-        | _ -> attribute_error ())
+        | ["value", "inversion"] -> Obj_class `InversionPrinciple
+	| _ -> attribute_error ())
   | tag ->
       match find_helm_exception ctxt with
       | Some (exn, arg) -> raise (Getter_failure (exn, arg))
@@ -751,6 +767,7 @@ let parse uri filename =
   | Failure "int_of_string" -> parse_error ctxt "integer number expected"
   | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected"
   | P.Parse_error msg -> parse_error ctxt ("parse error: " ^ msg)
+  | Sys.Break
   | Parser_failure _
   | Getter_failure _ as exn ->
       raise exn