From 18d6598d46ae02dc6fa0ecff8cd40798627033bd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 20:57:30 +0000 Subject: [PATCH] Cooking w.r.t. variables with bodies is now implemented as delta-expansion. --- helm/software/components/ng_kernel/oCic2NCic.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 0131b4311..cc675d276 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -384,9 +384,15 @@ let convert_term uri t = let ens,objs = List.fold_right (fun luri (l,objs) -> - let t = List.assoc luri ens in - let t,o = aux octx ctx n_fix uri t in - t::l, o@objs + match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph luri) with + Cic.Variable (_,bo,_,_,_) -> + let t = + match bo with + None -> List.assoc luri ens + | Some t -> CicSubstitution.subst_vars ens t in + let t,o = aux octx ctx n_fix uri t in + t::l, o@objs + | _ -> assert false ) params ([],[]) in NCic.Appl (he::ens),objs -- 2.39.2