]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/disambiguate.mli
Minor code reorganization:
[helm.git] / helm / gTopLevel / disambiguate.mli
index 63206cb154e31b3d272797366cedf68b89408d9f..2a03f58d997d22812192ce44ba30059a460295a0 100644 (file)
 (*                                                                            *)
 (******************************************************************************)
 
-(** Functions that should be moved in another module **)
-exception IllFormedUri of string
-val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string
-val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri
-
-val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string
-
 (** This module provides a functor to disambiguate the input **)
 (** given a set of user-interface call-backs                 **)
 
@@ -59,8 +52,7 @@ module type Callbacks =
 type domain_and_interpretation =
  string list * (string -> CicTextualParser0.uri option)
 
-module Make :
-  functor (C : Callbacks) ->
+module Make (C : Callbacks) :
     sig
       exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
       val disambiguate_input :