X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicParser.ml;h=e61ee78eabd1a8bed218b2d75d569e6a6bc53dd9;hb=419b8fd3c58efbcc5de030ee6b164dc93c5d83db;hp=3d1d3d1aa05ccbcd1ee313d8574b870b09fad3bd;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index 3d1d3d1aa..e61ee78ea 100644
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -296,23 +296,27 @@ let uri_list_of_string =
   fun s ->
     List.map uri_of_string (Str.split space_RE s)
 
+let impredicative_set = ref true;;
+
 let sort_of_string ctxt = function
   | "Prop" -> Cic.Prop
-  | "Set"  -> Cic.Set
   | "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 *)
   | "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";
-      try 
-        Cic.Type 
-          (CicUniv.fresh 
-            ~uri:ctxt.uri 
-            ~id:(int_of_string (String.sub s 5 (len - 5))) ())
+      let s = String.sub s 5 (len - 5) 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 uri = UriManager.uri_of_string suri in
+      try Cic.Type (CicUniv.fresh ~uri ~id ())
       with
       | Failure "int_of_string" 
       | Invalid_argument _ -> parse_error ctxt "sort expected" 
@@ -406,8 +410,15 @@ let end_element ctxt tag =
         | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
         | _ -> attribute_error ())
   | "def" ->  (* same as "decl" above *)
-      let ty = pop_cic ctxt in
-      let source = pop_cic ctxt in
+      let ty,source =
+       (*CSC: hack to parse Coq files where the LetIn is not typed *)
+       let ty = pop_cic ctxt in
+       try
+        let source = pop_cic ctxt in
+         ty,source
+       with
+        Parser_failure _ -> Cic.AImplicit ("MISSING_def_TYPE",None),ty
+      in
       push ctxt
         (match pop_tag_attrs ctxt with
         | ["binder", binder; "id", id]