From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 8 Apr 2008 21:18:03 +0000 (+0000)
Subject: Fix over the previous one: Var-LetIn abstractions should be ignored and not
X-Git-Tag: make_still_working~5391
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f8f187a75efdf72053738555ff7a18bf81a09c8d;p=helm.git

Fix over the previous one: Var-LetIn abstractions should be ignored and not
transformed into applications at all.
---

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index cc675d276..5a2fdb8f8 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -385,11 +385,9 @@ let convert_term uri t =
        List.fold_right
         (fun luri (l,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
+             Cic.Variable (_,Some _,_,_,_) -> l, objs
+           | Cic.Variable (_,None,_,_,_) ->
+              let t = List.assoc luri ens in
               let t,o = aux octx ctx n_fix uri t in
                t::l, o@objs
            | _ -> assert false