X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=05a15691eb3d478e7e8a0e986babac1adb7640db;hb=86af949158e013178557c7fec7662ac06fae753c;hp=0679b9aee634f2805bf61dca4f694cb4a4e07efe;hpb=108f7ef287b08d4d7228790d7c6d956434f16c6c;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 0679b9aee..05a15691e 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -631,7 +631,7 @@ module type Disambiguator =
 sig
   val disambiguate_term :
     ?fresh_instances:bool ->
-    dbd:Mysql.dbd ->
+    dbd:HMysql.dbd ->
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
@@ -646,7 +646,7 @@ sig
 
   val disambiguate_obj :
     ?fresh_instances:bool ->
-    dbd:Mysql.dbd ->
+    dbd:HMysql.dbd ->
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)