added attributes

[helm.git] / helm / ocaml / cic_omdoc / cic2content.ml

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index ef6999ca0887e65f5ad4036ca7320763d6693cda..aaf4512565e3ee30b479dc6b30c62efbb5021407 100644 (file)
--- 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;