made context and metasenv parameters of trivial disambiguator optional

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 1812285e044bc4c86308395114a942235deb13d6..54478c81a795862a8c89349a010ccd8ce954f5ae 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -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

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 4db990283b919825430810a363e28d5e0e390dda..3eff90ad67cb8df19ac3c93f2fb4f8bcb6d44948 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -53,8 +53,8 @@ sig
     * @raise Ambiguous_term for ambiguous term *)
   val disambiguate_string:
     dbd:Mysql.dbd ->
-    Cic.context ->
-    Cic.metasenv ->
+    ?context:Cic.context ->
+    ?metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
     ?aliases:environment ->         (* previous interpretation status *)
     string ->