X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=e93c54808298f14879396fbf637c3444c5bd775f;hb=ac741958783108ff31552e533c853e85c2ebb1c5;hp=64a469cabcb657f2f99a77056ba03b858897b811;hpb=47988107f44566d53fd5a71fd64a015bbf24a380;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 64a469cab..e93c54808 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -814,7 +814,7 @@ module type Disambiguator =
 sig
   val disambiguate_term :
     ?fresh_instances:bool ->
-    dbd:HMysql.dbd ->
+    dbd:HSql.dbd ->
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
@@ -829,7 +829,7 @@ sig
 
   val disambiguate_obj :
     ?fresh_instances:bool ->
-    dbd:HMysql.dbd ->
+    dbd:HSql.dbd ->
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)