The cache of objects is now used also for cofixpoints.

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 3880e361b9b9cbfbb19028b28022d1795ea396da..f16c1a98cfb0a90214bd2b3fe4474f1f7682d1d2 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