From f8f187a75efdf72053738555ff7a18bf81a09c8d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 21:18:03 +0000 Subject: [PATCH] Fix over the previous one: Var-LetIn abstractions should be ignored and not transformed into applications at all. --- helm/software/components/ng_kernel/oCic2NCic.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) 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 -- 2.39.2