X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=81f0683c6390530b1fabcb87437079084c79c77f;hb=0aaed6f96b856d1181a3cd1f2ef3ea4a91990771;hp=ef6999ca0887e65f5ad4036ca7320763d6693cda;hpb=4356006cb7b5fef3acbb9de7fabe14481e675f2e;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index ef6999ca0..81f0683c6 100644
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -374,10 +374,8 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
 			 CicEnvironment.get_obj CicUniv.empty_ugraph uri
 		       in
 			 match o with 
-                             Cic.Constant _ -> assert false
-			   | Cic.Variable _ -> assert false
-			   | Cic.CurrentProof _ -> assert false
-			   | Cic.InductiveDefinition (l,_,_) -> l 
+			   | Cic.InductiveDefinition (l,_,_,_) -> l 
+                           | _ -> assert false
                       ) in
                     let (_,_,_,constructors) = 
                       List.nth inductive_types tyno in 
@@ -548,7 +546,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
 		 Cic.Constant _ -> assert false
                | Cic.Variable _ -> assert false
                | Cic.CurrentProof _ -> assert false
-               | Cic.InductiveDefinition (l,_,n) -> l,n 
+               | Cic.InductiveDefinition (l,_,n,_) -> l,n 
           ) in
         let (_,_,_,constructors) = List.nth inductive_types typeno in
         let name_and_arities = 
@@ -694,10 +692,8 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
         let inductive_types,noparams =
           (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
 	     match o with
-		 Cic.Constant _ -> assert false
-               | Cic.Variable _ -> assert false
-               | Cic.CurrentProof _ -> assert false
-               | Cic.InductiveDefinition (l,_,n) -> (l,n) 
+               | Cic.InductiveDefinition (l,_,n,_) -> (l,n) 
+               | _ -> assert false
           ) in
         let rec split n l =
           if n = 0 then ([],l) else
@@ -916,7 +912,7 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
   let module C2A = Cic2acic in
   let seed = ref 0 in
   function
-      C.ACurrentProof (_,_,n,conjectures,bo,ty,params) ->
+      C.ACurrentProof (_,_,n,conjectures,bo,ty,params,_) ->
         (gen_id object_prefix seed, params,
           Some
            (List.map
@@ -925,27 +921,27 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
           `Def (K.Const,ty,
             build_def_item seed (get_id bo) (C.Name n) bo 
              ~ids_to_inner_sorts ~ids_to_inner_types))
-    | C.AConstant (_,_,n,Some bo,ty,params) ->
+    | C.AConstant (_,_,n,Some bo,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Def (K.Const,ty,
              build_def_item seed (get_id bo) (C.Name n) bo 
                ~ids_to_inner_sorts ~ids_to_inner_types))
-    | C.AConstant (id,_,n,None,ty,params) ->
+    | C.AConstant (id,_,n,None,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Decl (K.Const,
              build_decl_item seed id (C.Name n) ty 
                ~ids_to_inner_sorts))
-    | C.AVariable (_,n,Some bo,ty,params) ->
+    | C.AVariable (_,n,Some bo,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Def (K.Var,ty,
              build_def_item seed (get_id bo) (C.Name n) bo
                ~ids_to_inner_sorts ~ids_to_inner_types))
-    | C.AVariable (id,n,None,ty,params) ->
+    | C.AVariable (id,n,None,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Decl (K.Var,
              build_decl_item seed id (C.Name n) ty
               ~ids_to_inner_sorts))
-    | C.AInductiveDefinition (id,l,params,nparams) ->
+    | C.AInductiveDefinition (id,l,params,nparams,_) ->
          (gen_id object_prefix seed, params, None,
             `Joint
               { K.joint_id = gen_id joint_prefix seed;
@@ -959,6 +955,7 @@ and
       fun (_,n,b,ty,l) ->
         `Inductive
           { K.inductive_id = gen_id inductive_prefix seed;
+            K.inductive_name = n;
             K.inductive_kind = b;
             K.inductive_type = ty;
             K.inductive_constructors = build_constructors seed l