From c9515ad8b94542e3164ab6affddef5ae3129f2e4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Apr 2008 13:14:45 +0000 Subject: [PATCH 1/1] added translation of Set to Type0 (avoid warning) --- helm/software/components/ng_kernel/oCic2NCic.ml | 1 + 1 file changed, 1 insertion(+) 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 = -- 2.39.2