MQueryInterpreter: interface updated

[helm.git] / helm / gTopLevel / disambiguate.mli

diff --git a/helm/gTopLevel/disambiguate.mli b/helm/gTopLevel/disambiguate.mli
index 40ad3ec2e97a02d184230568d7fcaa14d4778d3f..9fdfb8993dae6cdf8eaf7c57a97414d96259955b 100644 (file)
--- a/helm/gTopLevel/disambiguate.mli
+++ b/helm/gTopLevel/disambiguate.mli
@@ -63,6 +63,7 @@ module Make (C : Callbacks) :
     sig
       exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
       val disambiguate_input :
+        MQIConn.handle -> 
         Cic.context ->
         Cic.metasenv ->
         CicTextualParser0.interpretation_domain_item list ->