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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 535509a88..b9c053653 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 let nonvar uri = not (UriManager.uri_is_var uri)
@@ -170,7 +172,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 +190,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