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

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 56459d197..81f0683c6 100644
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -294,26 +294,28 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_
 
 let build_decl_item seed id n s ~ids_to_inner_sorts =
  let module K = Content in
-  try
-   let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in
-   if sort = "Prop" then
-      `Hypothesis
-        { K.dec_name = name_of n;
-          K.dec_id = gen_id declaration_prefix seed; 
-          K.dec_inductive = false;
-          K.dec_aref = id;
-          K.dec_type = s
-        }
-   else 
-      `Declaration
-        { K.dec_name = name_of n;
-          K.dec_id = gen_id declaration_prefix seed; 
-          K.dec_inductive = false;
-          K.dec_aref = id;
-          K.dec_type = s
-        }
-  with
-   Not_found -> assert false
+ let sort =
+   try
+    Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id))
+   with Not_found -> None
+ in
+ match sort with
+ | Some "Prop" ->
+    `Hypothesis
+      { K.dec_name = name_of n;
+        K.dec_id = gen_id declaration_prefix seed; 
+        K.dec_inductive = false;
+        K.dec_aref = id;
+        K.dec_type = s
+      }
+ | _ ->
+    `Declaration
+      { K.dec_name = name_of n;
+        K.dec_id = gen_id declaration_prefix seed; 
+        K.dec_inductive = false;
+        K.dec_aref = id;
+        K.dec_type = s
+      }
 ;;
 
 let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts =
@@ -369,13 +371,11 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  if sort ="Prop" then 
                     let inductive_types =
                       (let o,_ = 
-			 CicEnvironment.get_obj uri CicUniv.empty_ugraph 
+			 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 
@@ -541,12 +541,12 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
         let inductive_types,noparams =
-          (let o, _ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+          (let o, _ = 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,_,n) -> l,n 
+               | Cic.InductiveDefinition (l,_,n,_) -> l,n 
           ) in
         let (_,_,_,constructors) = List.nth inductive_types typeno in
         let name_and_arities = 
@@ -690,12 +690,10 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
         let ind_str = (prefix ^ ".ind") in 
         let ind_uri = UriManager.uri_of_string ind_str in
         let inductive_types,noparams =
-          (let o,_ = CicEnvironment.get_obj ind_uri CicUniv.empty_ugraph in
+          (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
@@ -914,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
@@ -923,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;
@@ -957,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