From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 8 Apr 2008 20:57:30 +0000 (+0000)
Subject: Cooking w.r.t. variables with bodies is now implemented as delta-expansion.
X-Git-Tag: make_still_working~5393
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18d6598d46ae02dc6fa0ecff8cd40798627033bd;p=helm.git

Cooking w.r.t. variables with bodies is now implemented as delta-expansion.
---

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