From cc0999086c1f4485da1afa752f3e111fb37ce001 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 18 Apr 2008 16:50:10 +0000 Subject: [PATCH 1/1] workaround for some Set/Type problems --- helm/software/components/ng_kernel/oCic2NCic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 4aaeb414c..320df7c9f 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -497,7 +497,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 u) -> - NCic.Sort (NCic.Type (CicUniv.get_rank u)),[] + NCic.Sort (NCic.Type (CicUniv.get_rank u+1)),[] | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type 0),[] (* calculate depth in the univ_graph*) | Cic.Appl l -> -- 2.39.2