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
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