From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 2 Apr 2008 13:14:45 +0000 (+0000)
Subject: added translation of Set to Type0 (avoid warning)
X-Git-Tag: make_still_working~5468
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=c9515ad8b94542e3164ab6affddef5ae3129f2e4;hp=04d8e2282a3536a9b822a8dbfcbdb4e3a949f04d;p=helm.git

added translation of Set to Type0 (avoid warning)
---

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index ac9ba639a..b2591b361 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -184,6 +184,7 @@ let convert_term uri t =
     | Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
     | Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
     | Cic.Sort (Cic.Type _) -> NCic.Sort (NCic.Type 0),[] 
+    | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type 0),[] 
        (* calculate depth in the univ_graph*)
     | Cic.Appl l -> 
         let l, fixpoints =