From f233a527ff4233ae9dc948550b0b5adef16696e0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 10 Apr 2008 18:19:16 +0000 Subject: [PATCH] The cache of objects is now used also for cofixpoints. --- helm/software/components/ng_kernel/oCic2NCic.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 3880e361b..f16c1a98c 100644 --- 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 -- 2.39.2