Implemented translation of inductive types from the new to the old format.

diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml
index d78d5f3fe33c663d3f6504ec6d04deb34f0bcfa8..e67e1ba90f0e6f98e2f6a08562d3721a48149473 100644 (file)
--- 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,[])]
 ;;