From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 19 Apr 2008 16:26:21 +0000 (+0000)
Subject: added flag to change Set into Type on the fly, that helps on some coq objects using... 
X-Git-Tag: make_still_working~5314
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9b9f415916ff4842c69f4918064d5dd64031df63;p=helm.git

added flag to change Set into Type on the fly, that helps on some coq objects using impredicative set
---

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index 9fac7badb..0f36f1a04 100644
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -296,14 +296,17 @@ 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";
diff --git a/helm/software/components/cic/cicParser.mli b/helm/software/components/cic/cicParser.mli
index 9472b4c54..d874293a1 100644
--- a/helm/software/components/cic/cicParser.mli
+++ b/helm/software/components/cic/cicParser.mli
@@ -44,3 +44,4 @@ val annobj_of_xml: UriManager.uri -> string -> string option -> Cic.annobj
    * Both files are assumed to be gzipped. *)
 val obj_of_xml : UriManager.uri -> string -> string option -> Cic.obj
 
+val impredicative_set : bool ref