parameter sintax added to axiom statement

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

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index 30e7a0b38903385fdee48dee1dbc28a0458e4467..3962323a18767d0faa087f486b44d768cbfa901e 100644 (file)
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -694,13 +694,6 @@ 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 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)