.ma inclusions corrected/minimized

[helm.git] / helm / matita / matitaDisambiguator.mli

diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli
index 740de989ecfa027c3c73a0e1f63c8355b1f7dafd..01fa97ef08810b9741a4efa6ebcaaac80152a86e 100644 (file)
--- a/helm/matita/matitaDisambiguator.mli
+++ b/helm/matita/matitaDisambiguator.mli
@@ -48,7 +48,3 @@ val mono_interp_callback: choose_interp_callback
 (** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *)
 
 include Disambiguate.Disambiguator
-  (*
-   * val disambiguate_term: ...
-   *)
-