]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.ml
made context and metasenv parameters of trivial disambiguator optional
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml
index 1812285e044bc4c86308395114a942235deb13d6..54478c81a795862a8c89349a010ccd8ce954f5ae 100644 (file)
@@ -621,8 +621,8 @@ struct
     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 disambiguate_string ~dbd ?(context=[]) ?(metasenv=[]) ?initial_ugraph
+        ?(aliases=DisambiguateTypes.Environment.empty) term =
     let ast = CicTextualParser2.parse_term (Stream.of_string term) in
     try
       Disambiguator.disambiguate_term ~dbd context metasenv ast ?initial_ugraph