From 18ee8c139d1fd56d34b97e6b417c0f14d9417886 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 08:16:55 +0000 Subject: [PATCH] Implemented translation of inductive types from the new to the old format. --- helm/software/components/ng_kernel/nCic2OCic.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml index d78d5f3fe..e67e1ba90 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.ml +++ b/helm/software/components/ng_kernel/nCic2OCic.ml @@ -100,5 +100,13 @@ let convert_nobj = function convert_term u 0 (let _,_,_,ty,_ = List.hd fl in ty), [], [])) (let rec seq = function 0 -> [0]|n -> n::seq (n-1) in seq (List.length fl-1)) - | _,_,_,_,NCic.Inductive _ -> assert false + | u,_,_,_,NCic.Inductive (inductive,leftno,itl,_) -> + let itl = + List.map + (function (_,name,ty,cl) -> + let cl=List.map (function (_,name,ty) -> name,convert_term u 0 ty) cl in + name,inductive,convert_term u 0 ty,cl + ) itl + in + [ouri_of_nuri u, Cic.InductiveDefinition (itl,[],leftno,[])] ;; -- 2.39.2