New module HMysql (to abstract over Mysql and make profiling easier).

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.mli

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 1c6d4bbe7d3e3002462b237a7b6b93aa36a5e736..356b5e117274f570634e15167c07ad810d76d2d5 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -39,7 +39,7 @@ sig
    * input AST will be ignored. Defaults to false. *)
   val disambiguate_term :
     ?fresh_instances:bool ->
-    dbd:Mysql.dbd ->
+    dbd:HMysql.dbd ->
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
@@ -55,7 +55,7 @@ sig
   (** @param fresh_instances as per disambiguate_term *)
   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 *)
@@ -77,7 +77,7 @@ sig
     * choice from the user is needed to disambiguate the term
     * @raise Ambiguous_term for ambiguous term *)
   val disambiguate_string:
-    dbd:Mysql.dbd ->
+    dbd:HMysql.dbd ->
     ?context:Cic.context ->
     ?metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph ->