more strings to UriManager.uri

[helm.git] / helm / ocaml / tactics / metadataQuery.ml

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 644e764ef56c18b927777d013cfc6a0dd8bebd3d..c1dd20ecc83badb808fb8e303b7feec3d701bbbf 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -211,7 +211,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
 (*                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 =
@@ -242,7 +242,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
 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
@@ -281,7 +281,7 @@ let experimental_hint
       | 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
@@ -313,7 +313,7 @@ let experimental_hint
               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 =
@@ -484,7 +484,9 @@ let fwd_simpl ~dbd t =
    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) = 
@@ -505,7 +507,9 @@ let fwd_simpl ~dbd t =
       | 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