From 4164d93a5e0ac9c6d66dde4c88b3302b01fda743 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Apr 2008 15:13:47 +0000 Subject: [PATCH] use universe rank instead of Type0 --- helm/software/components/ng_kernel/oCic2NCic.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index f16c1a98c..876f6a261 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -462,7 +462,8 @@ let convert_term uri t = NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty | 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.Type u) -> + NCic.Sort (NCic.Type (CicUniv.get_rank u)),[] | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type 0),[] (* calculate depth in the univ_graph*) | Cic.Appl l -> -- 2.39.2