X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser.ml;h=317bcb9f0a002f17284133d3da7c9bdd972c2116;hb=acd31bfb9537bd32781404241c80bd0ebf88e3b1;hp=887ed975f74f00a5ffff420e9f46eb201042a15d;hpb=c8a5bd44cf3de45e2736d45bfb8b9b23835b309b;p=helm.git

diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml
index 887ed975f..317bcb9f0 100644
--- a/helm/ocaml/cic/cicParser.ml
+++ b/helm/ocaml/cic/cicParser.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s)
 
@@ -297,10 +299,23 @@ let uri_list_of_string =
 let sort_of_string ctxt = function
   | "Prop" -> Cic.Prop
   | "Set"  -> Cic.Set
-  | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
-(*   | "Type" -> CicUniv.restart_numbering (); |+ useful only to test parser +| *)
   | "CProp" -> Cic.CProp
-  | _ -> parse_error ctxt "sort expected"
+  (* 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 *)
+  | "Type" ->  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";
+      try 
+        Cic.Type 
+          (CicUniv.fresh 
+            ~uri:ctxt.uri 
+            ~id:(int_of_string (String.sub s 5 (len - 5))) ())
+      with
+      | Failure "int_of_string" 
+      | Invalid_argument _ -> parse_error ctxt "sort expected" 
 
 let patch_subst ctxt subst = function
   | Cic.AConst (id, uri, _) -> Cic.AConst (id, uri, subst)
@@ -673,7 +688,13 @@ let end_element ctxt tag =
             let fields =
               List.map
                 (function
-                  | Obj_field name -> name
+                  | Obj_field name -> 
+                      (match Str.split (Str.regexp " ") name with
+                      | [name] -> name, false
+                      | [name;"coercion"] -> name,true
+                      | _ -> 
+                          parse_error
+                            "wrong \"field\"'s name attribute")
                   | _ ->
                       parse_error
                         "unexpected extra content for \"record\" object class")