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 0131b43119a31b5ad37553a4c4fe40a32d5255d6..cc675d2768eca313934f6db3082322c31ad37331 100644 (file)
--- 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