X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=49e2e23ad11e738442faa10d8dca38c597ba937a;hb=bb236c2ac110124de92fa2d0fb2882d273a7f7eb;hp=eac04e7aa4919b17d6eb94aec555b77a2d2ff3de;hpb=2e062d07e358eb95f0dcbec8fcdfbc2a4fb9ae1f;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index eac04e7aa..49e2e23ad 100644
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -70,7 +70,7 @@ let rec occur uri =
     | C.Var _ -> false
     | C.Meta _ -> false
     | C.Sort _ -> false
-    | C.Implicit -> raise NotImplemented
+    | C.Implicit _ -> assert false
     | C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
     | C.Cast (te,ty) -> (occur uri te)
     | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)
@@ -678,10 +678,9 @@ 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 
@@ -790,9 +789,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