From a2642c03bef7812ca81b25da0d3cb2f504e0a0b0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 15:56:31 +0000 Subject: [PATCH] The old kernel does not accept ens whose order is different from the one declared for the object whose reference it is applied to. Fixed. --- .../components/ng_kernel/oCic2NCic.ml | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 3493dbff5..f54f184d8 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -315,20 +315,29 @@ let convert_term uri t = ;; let cook mode vars t = - let t = CicSubstitution.lift (List.length vars) t in - List.fold_right - (fun uri t -> - let t = CicSubstitution.subst_vars [uri,Cic.Rel 1] t in + let varsno = List.length vars in + let t = CicSubstitution.lift varsno t in + let rec aux n acc l = + let subst = + snd(List.fold_left (fun (i,res) uri -> i+1,(uri,Cic.Rel i)::res) (1,[]) acc) + in + match l with + [] -> CicSubstitution.subst_vars subst t + | uri::uris -> let bo,ty = match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with Cic.Variable (_,bo,ty,_,_) -> bo,ty | _ -> assert false in + let ty = CicSubstitution.subst_vars subst ty in + let bo = HExtlib.map_option (CicSubstitution.subst_vars subst) bo in let id = Cic.Name (UriManager.name_of_uri uri) in + let t = aux (n-1) (uri::acc) uris in match bo,ty,mode with None,ty,`Lambda -> Cic.Lambda (id,ty,t) | None,ty,`Pi -> Cic.Prod (id,ty,t) | Some bo,ty,_ -> Cic.LetIn (id,bo,ty,t) - ) vars t + in + aux varsno [] vars ;; let convert_obj_aux uri = function -- 2.39.2