if n<0 then raise NotApplicable
else
let method_name =
- if uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" then
- "Exists"
+ 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 "ByInduction" in
let prefix = String.sub uri_str 0 n in
let ind_str = (prefix ^ ".ind") in