X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FmetadataQuery.ml;h=abe192b94b9341b98ac05647c27985517bdabb91;hb=refs%2Ftags%2F0.4.95%407852;hp=6b87de349ce7f2225b54835e968b6cb54c7d6463;hpb=fbdd1cc46819d19ed135391a4a954c19d1b92c0c;p=helm.git

diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml
index 6b87de349..abe192b94 100644
--- a/components/tactics/metadataQuery.ml
+++ b/components/tactics/metadataQuery.ml
@@ -194,7 +194,7 @@ let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
 let cmatch' = Constr.cmatch'
 
 (* used only by te old auto *)
-let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
+let signature_of_goal ~(dbd:HSql.dbd) ((proof, goal) as _status) =
  let (_, metasenv, _subst, _, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in
@@ -275,7 +275,7 @@ let signature_of metasenv goal =
     close_with_types set metasenv context
 
 
-let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal =
+let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let ty_set = Constr.constants_of ty in
   let hyp_set = signature_of_hypothesis context metasenv in
@@ -334,7 +334,7 @@ let filter_out_predicate set ctx menv =
   Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set  
 ;;
 
-let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
+let equations_for_goal ~(dbd:HSql.dbd) ?signature ((proof, goal) as _status) =
 (*
   let to_string set =
     "{\n" ^
@@ -393,7 +393,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
    (*        else raise Goal_is_not_an_equation *)
 
 let experimental_hint 
-  ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
+  ~(dbd:HSql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let (_, metasenv, _subst, _, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
@@ -475,7 +475,7 @@ let experimental_hint
     (aux uris)
 
 let new_experimental_hint 
-  ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
+  ~(dbd:HSql.dbd) ?(facts=false) ?signature ~universe
   ((proof, goal) as status)
 =
   let (_, metasenv,  _subst, _, _, _) = proof in