From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 18 May 2008 08:16:55 +0000 (+0000)
Subject: Implemented translation of inductive types from the new to the old format.
X-Git-Tag: make_still_working~5172
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18ee8c139d1fd56d34b97e6b417c0f14d9417886;p=helm.git

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 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,[])]
 ;;