removed deadcode / fixed typos (thanks to ocaml 3.09)

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 535509a88afd0221b89ae49278373ecb2f948f2b..9385f1c99d3ef3cef1845f82a05dac3707c011b9 100644 (file)
--- 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