From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 22 Apr 2005 15:24:31 +0000 (+0000)
Subject: made context and metasenv parameters of trivial disambiguator optional
X-Git-Tag: after_svn_merge~20
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d8dd9228da904dd64317ef87e0f1b499af8606ba;p=helm.git

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 1812285e0..54478c81a 100644
--- 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 4db990283..3eff90ad6 100644
--- 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 ->