BIG FAT COMMIT REGARDING COERCIONS:

[helm.git] / components / cic / cicParser.ml

diff --git a/components/cic/cicParser.ml b/components/cic/cicParser.ml
index 1e9a3a33c1444a553f9b7beaa8b5bee709a58254..150fe4ad983f6dab3bad1d117877e6093531b755 100644 (file)
--- a/components/cic/cicParser.ml
+++ b/components/cic/cicParser.ml
@@ -678,7 +678,13 @@ let end_element ctxt tag =
       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)
@@ -691,8 +697,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")