From d8dd9228da904dd64317ef87e0f1b499af8606ba Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Apr 2005 15:24:31 +0000 Subject: [PATCH] made context and metasenv parameters of trivial disambiguator optional --- helm/ocaml/cic_disambiguation/disambiguate.ml | 4 ++-- helm/ocaml/cic_disambiguation/disambiguate.mli | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) 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 -> -- 2.39.2