X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=81f0683c6390530b1fabcb87437079084c79c77f;hb=2f15a81dcd6e5ada3f1b4fa6300e9a1347c8d12c;hp=61003f930fbca68abc1515a78acf92122659e9d2;hpb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 61003f930..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 =
@@ -368,11 +370,12 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                     with Not_found -> "Type") in 
                  if sort ="Prop" then 
                     let inductive_types =
-                      (match CicEnvironment.get_obj uri with
-                         Cic.Constant _ -> assert false
-                       | Cic.Variable _ -> assert false
-                       | Cic.CurrentProof _ -> assert false
-                       | Cic.InductiveDefinition (l,_,_) -> l 
+                      (let o,_ = 
+			 CicEnvironment.get_obj CicUniv.empty_ugraph uri
+		       in
+			 match o with 
+			   | Cic.InductiveDefinition (l,_,_,_) -> l 
+                           | _ -> assert false
                       ) in
                     let (_,_,_,constructors) = 
                       List.nth inductive_types tyno in 
@@ -538,12 +541,13 @@ 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 =
-           (match CicEnvironment.get_obj uri with
-               Cic.Constant _ -> assert false
-             | Cic.Variable _ -> assert false
-             | Cic.CurrentProof _ -> assert false
-             | Cic.InductiveDefinition (l,_,n) -> l,n 
-           ) 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 
+          ) in
         let (_,_,_,constructors) = List.nth inductive_types typeno in
         let name_and_arities = 
           let rec count_prods =
@@ -678,21 +682,19 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
       if n<0 then raise NotApplicable
       else 
         let method_name =
-          if (uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" or
-              uri_str = "cic:/Coq/Init/Logic/ex_ind.con") then "Exists"
-          else if uri_str = "cic:/Coq/Init/Logic/and_ind.con" then "AndInd"
-          else if uri_str = "cic:/Coq/Init/Logic/False_ind.con" then "FalseInd"
+          if UriManager.eq uri HelmLibraryObjects.Logic.ex_ind_URI then "Exists"
+          else if UriManager.eq uri HelmLibraryObjects.Logic.and_ind_URI then "AndInd"
+          else if UriManager.eq uri HelmLibraryObjects.Logic.false_ind_URI then "FalseInd"
           else "ByInduction" in
         let prefix = String.sub uri_str 0 n in
         let ind_str = (prefix ^ ".ind") in 
         let ind_uri = UriManager.uri_of_string ind_str in
         let inductive_types,noparams =
-           (match CicEnvironment.get_obj ind_uri with
-               Cic.Constant _ -> assert false
-             | Cic.Variable _ -> assert false
-             | Cic.CurrentProof _ -> assert false
-             | Cic.InductiveDefinition (l,_,n) -> (l,n) 
-           ) in
+          (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
+	     match o with
+               | Cic.InductiveDefinition (l,_,n,_) -> (l,n) 
+               | _ -> assert false
+          ) in
         let rec split n l =
           if n = 0 then ([],l) else
           let p,a = split (n-1) (List.tl l) in
@@ -790,9 +792,8 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
   let module C = Cic in
   match li with 
     C.AConst (sid,uri,exp_named_subst)::args ->
-      let uri_str = UriManager.string_of_uri uri in
-      if uri_str = "cic:/Coq/Init/Logic/eq_ind.con" or
-         uri_str = "cic:/Coq/Init/Logic/eq_ind_r.con" then 
+      if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI or
+         UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_r_URI then 
         let subproofs,arg = 
           (match 
              build_subproofs_and_args 
@@ -911,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
@@ -920,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;
@@ -954,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