added depndency of new kernel to metadata to allow to use the DB to calculate the...

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 3880e361b9b9cbfbb19028b28022d1795ea396da..876f6a261670692977b2cb34d1d50726bcdfcffc 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -321,7 +321,10 @@ let convert_term uri t =
      preceed its lefts parameters; in the former case, there is nothing to
      permute *)
   let rec aux k octx (ctx : ctx list) n_fix uri = function
-    | Cic.CoFix (cofixno, fl) ->
+    | Cic.CoFix _ as cofix ->
+        let octx,ctx,fix,rels = restrict octx ctx cofix in
+        let cofixno,fl =
+         match fix with Cic.CoFix (cofixno,fl)->cofixno,fl | _-> assert false in
         let buri = 
           UriManager.uri_of_string 
            (UriManager.buri_of_uri uri^"/"^
@@ -359,7 +362,7 @@ let convert_term uri t =
         in
         splat_args ctx 
          (NCic.Const (Ref.reference_of_ouri buri (Ref.CoFix cofixno)))
-         n_fix (assert false),
+         n_fix rels,
         fixpoints @ [obj]
     | Cic.Fix _ as fix ->
         let octx,ctx,fix,rels = restrict octx ctx fix in
@@ -459,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 ->