(* debug_print ("STO APPLICANDO " ^ uri); *)
PET.apply_tactic
(PrimitiveTactics.apply_tac
- ~term:(CicUtil.term_of_uri (UriManager.string_of_uri uri)))
+ ~term:(CicUtil.term_of_uri uri))
status
in
let goal_list =
let close_with_types s metasenv context =
Constr.UriManagerSet.fold
(fun e bag ->
- let t = CicUtil.term_of_uri (UriManager.string_of_uri e) in
+ let t = CicUtil.term_of_uri e in
let ty, _ =
CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph
in
| Some (main,_) ->
let ty, _ =
CicTypeChecker.type_of_aux'
- metasenv context (CicUtil.term_of_uri (UriManager.string_of_uri main)) CicUniv.empty_ugraph
+ metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
in
Constr.constants_of ty
in
let (subst,(proof, goal_list)) =
(* debug_print ("STO APPLICANDO" ^ uri); *)
PrimitiveTactics.apply_tac_verbose
- ~term:(CicUtil.term_of_uri (UriManager.string_of_uri uri))
+ ~term:(CicUtil.term_of_uri uri)
status
in
let goal_list =
let map inners row =
match row.(0), row.(1), row.(2) with
| Some source, Some inner, Some index ->
- source, List.mem (int_of_string index, inner) inners
+ source,
+ List.mem
+ (int_of_string index, (UriManager.uri_of_string inner)) inners
| _ -> "", false
in
let rec rank ranks (source, ok) =
| Some (outer, inners) ->
let select = "source, h_inner, h_index" in
let from = "genLemma" in
- let where = Printf.sprintf "h_outer = \"%s\"" (Mysql.escape outer) in
+ let where =
+ Printf.sprintf "h_outer = \"%s\""
+ (Mysql.escape (UriManager.string_of_uri outer)) in
let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in
let result = Mysql.exec dbd query in
let lemmas = Mysql.map result ~f:(map inners) in