changed META dependency

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

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index e69099cb5d30dda0527de4f4403c4e8727de3255..3e6ce26e7c5a56971cd6e1369b516b0eb7daba16 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -947,28 +947,3 @@ in refine_profiler.HExtlib.profile foo ()
         obj
   end
 
-module Trivial =
-struct
-  exception Ambiguous_term of string Lazy.t
-  exception Exit
-  module Callbacks =
-  struct
-    let interactive_user_uri_choice ~selection_mode ?ok
-          ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
-              raise Exit
-    let interactive_interpretation_choice interp = raise Exit
-    let input_or_locate_uri ~(title:string) ?id = raise Exit
-  end
-  module Disambiguator = Make (Callbacks)
-  let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph
-    ?(aliases = DisambiguateTypes.Environment.empty) term
-  =
-    let ast =
-      CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term)
-    in
-    try
-      fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
-        ?initial_ugraph ~aliases ~universe:None)
-    with Exit -> raise (Ambiguous_term (lazy term))
-end
-