X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=9385f1c99d3ef3cef1845f82a05dac3707c011b9;hb=d0c88a989d2c41d0b816c5490d4d8c89a238cb2a;hp=535509a88afd0221b89ae49278373ecb2f948f2b;hpb=6203a9d0d56c7ec7cd11713b5ed56645271154be;p=helm.git

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 535509a88..9385f1c99 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -170,7 +170,7 @@ let cmatch' =
 let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
 let cmatch' = Constr.cmatch'
 
-let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
+let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
  let (_, metasenv, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in
@@ -188,14 +188,14 @@ let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
   uris
 
-let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
-  let to_string set =
+let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
+(*   let to_string set =
     "{ " ^
       (String.concat ", "
          (Constr.UriManagerSet.fold
             (fun u l -> (UriManager.string_of_uri u)::l) set []))
     ^ " }"
-  in
+  in *)
  let (_, metasenv, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in