From b059fe5ee46d45bc2985b0f46f6a69b4b3be248b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 25 Mar 2008 15:51:59 +0000 Subject: [PATCH] ported to the Cic LetIn with explicit type --- helm/software/components/ng_kernel/nCic2OCic.ml | 4 ++-- helm/software/components/ng_kernel/oCic2NCic.ml | 15 ++++++--------- 2 files changed, 8 insertions(+), 11 deletions(-) diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml index 3f735a824..d7011c8df 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.ml +++ b/helm/software/components/ng_kernel/nCic2OCic.ml @@ -12,8 +12,8 @@ let convert_term uri n_fl t = Cic.Prod (nn_2_on n,convert_term k s, convert_term (k+1) t) | NCic.Lambda (n,s,t) -> Cic.Lambda(nn_2_on n,convert_term k s, convert_term (k+1) t) - | NCic.LetIn (n,_,s,t) -> - Cic.LetIn (nn_2_on n,convert_term k s, convert_term (k+1) t) + | NCic.LetIn (n,ty_s,s,t) -> + Cic.LetIn (nn_2_on n,convert_term k s,convert_term k ty_s, convert_term (k+1) t) | NCic.Sort NCic.Prop -> Cic.Sort Cic.Prop | NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp | NCic.Sort NCic.Set -> Cic.Sort Cic.Set diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 1d0e453b0..2f95d663c 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -169,16 +169,13 @@ let convert_term uri t = let octx = Some (name, Cic.Decl old_s) :: octx in let t, fixpoints_t = aux octx ctx n_fix uri t in NCic.Prod (cn_to_s name, s, t), fixpoints_s @ fixpoints_t - | Cic.LetIn (name, (s as old_s), t) -> - let s, fixpoints_s = aux octx ctx n_fix uri s in - let old_ty,_ = - CicTypeChecker.type_of_aux' [] octx old_s CicUniv.oblivion_ugraph - in - let ty, fixpoints_ty = aux octx ctx n_fix uri old_ty in - let ctx = Ce (cn_to_s name, NCic.Def (s, ty)) :: ctx in - let octx = Some (name, Cic.Def (old_s, Some old_ty)) :: octx in + | Cic.LetIn (name, (te as old_te), (ty as old_ty), t) -> + let te, fixpoints_s = aux octx ctx n_fix uri te in + let ty, fixpoints_ty = aux octx ctx n_fix uri ty in + let ctx = Ce (cn_to_s name, NCic.Def (te, ty)) :: ctx in + let octx = Some (name, Cic.Def (old_te, old_ty)) :: octx in let t, fixpoints_t = aux octx ctx n_fix uri t in - NCic.LetIn (cn_to_s name, ty, s, t), + NCic.LetIn (cn_to_s name, ty, te, t), fixpoints_s @ fixpoints_t @ fixpoints_ty | Cic.Cast (t,ty) -> let t, fixpoints_t = aux octx ctx n_fix uri t in -- 2.39.2