made context and metasenv parameters of trivial disambiguator optional

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

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 ->