From cf99d74ebb4a2d20adef98e5e13340a00791ebef Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 21:31:13 +0000 Subject: [PATCH] Variables having a body can occur in cooked terms and must be delta-expanded during translation to the new CIC format. --- helm/software/components/ng_kernel/oCic2NCic.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 5a2fdb8f8..5b4d9f9e1 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -357,6 +357,11 @@ let convert_term uri t = | Cic.MutConstruct (curi, tyno, consno, ens) -> aux_ens curi octx ctx n_fix uri ens (NCic.Const (Ref.reference_of_ouri curi (Ref.Con (tyno,consno)))) + | Cic.Var (curi, ens) -> + (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with + Cic.Variable (_,Some bo,_,_,_) -> + aux octx ctx n_fix uri (CicSubstitution.subst_vars ens bo) + | _ -> assert false) | Cic.MutCase (curi, tyno, outty, t, branches) -> let r = Ref.reference_of_ouri curi (Ref.Ind tyno) in let outty, fixpoints_outty = aux octx ctx n_fix uri outty in @@ -369,7 +374,7 @@ let convert_term uri t = branches ([],[]) in NCic.Match (r,outty,t,branches), fixpoints_outty@fixpoints_t@fixpoints - | Cic.Implicit _ | Cic.Meta _ | Cic.Var _ -> assert false + | Cic.Implicit _ | Cic.Meta _ -> assert false and aux_ens curi octx ctx n_fix uri ens he = match ens with [] -> he,[] -- 2.39.2