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 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