From 9b9f415916ff4842c69f4918064d5dd64031df63 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 19 Apr 2008 16:26:21 +0000 Subject: [PATCH] added flag to change Set into Type on the fly, that helps on some coq objects using impredicative set --- helm/software/components/cic/cicParser.ml | 5 ++++- helm/software/components/cic/cicParser.mli | 1 + 2 files changed, 5 insertions(+), 1 deletion(-) 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 -- 2.39.2