X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicParser.ml;h=3962323a18767d0faa087f486b44d768cbfa901e;hb=7f9e313fe5ae4200f080f481a6b8b795a0618093;hp=e61ee78eabd1a8bed218b2d75d569e6a6bc53dd9;hpb=c031aa4ca97d0d563a772d7bd247ff7814c51b04;p=helm.git

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index e61ee78ea..3962323a1 100644
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -300,23 +300,26 @@ let impredicative_set = ref true;;
 
 let sort_of_string ctxt = function
   | "Prop" -> Cic.Prop
-  | "CProp" -> Cic.CProp
   (* THIS CASE IS HERE ONLY TO ALLOW THE PARSING OF COQ LIBRARY
    * THIS SHOULD BE REMOVED AS SOON AS univ_maker OR COQ'S EXPORTATION 
    * IS FIXED *)
+  | "CProp" -> Cic.CProp (CicUniv.fresh ~uri:ctxt.uri ())
   | "Type" ->  Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
   | "Set" when !impredicative_set -> Cic.Set
   | "Set" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
   | s ->
       let len = String.length s in
-      if not(len > 5) then parse_error ctxt "sort expected";
-      if not(String.sub s 0 5 = "Type:") then parse_error ctxt "sort expected";
-      let s = String.sub s 5 (len - 5) in
+      let sort_len, mk_sort = 
+        if len > 5 && String.sub s 0 5 = "Type:" then 5,fun x -> Cic.Type x 
+        else if len > 6 && String.sub s 0 6 = "CProp:" then 6,fun x->Cic.CProp x
+        else parse_error ctxt "sort expected"
+      in
+      let s = String.sub s sort_len (len - sort_len) in
       let i = String.index s ':' in  
       let id =  int_of_string (String.sub s 0 i) in
-      let suri = String.sub s (i+1) (len - 5 - i - 1) in
+      let suri = String.sub s (i+1) (len - sort_len - i - 1) in
       let uri = UriManager.uri_of_string suri in
-      try Cic.Type (CicUniv.fresh ~uri ~id ())
+      try mk_sort (CicUniv.fresh ~uri ~id ())
       with
       | Failure "int_of_string" 
       | Invalid_argument _ -> parse_error ctxt "sort expected" 
@@ -691,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)