X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=c1dd20ecc83badb808fb8e303b7feec3d701bbbf;hb=c0f06261e5626228e4681de9973b6412524f09a2;hp=644e764ef56c18b927777d013cfc6a0dd8bebd3d;hpb=a7b90d2494f7d580faa54ecd2835bd4649129763;p=helm.git

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 644e764ef..c1dd20ecc 100644
--- 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