From f44a2623c7790b8ad052e967c008869ab017d7e9 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 27 Apr 2005 17:25:58 +0000 Subject: [PATCH] bugfix: patched .ml.in instaned of .ml :-( --- helm/gTopLevel/disambiguatingParser.ml.in | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/gTopLevel/disambiguatingParser.ml.in b/helm/gTopLevel/disambiguatingParser.ml.in index 224eb4b6e..c3302c8b9 100644 --- a/helm/gTopLevel/disambiguatingParser.ml.in +++ b/helm/gTopLevel/disambiguatingParser.ml.in @@ -31,14 +31,15 @@ module AndreaAndZackDisambiguatingParser = module Make (C : DisambiguateTypes.Callbacks) = struct - let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term_as_string - aliases + let disambiguate_term ~(dbd:Mysql.dbd) ~context ~metasenv + ?initial_ugraph ~aliases term_as_string = let module Disambiguate' = Disambiguate.Make (C) in let term = CicTextualParser2.parse_term (Stream.of_string term_as_string) in - Disambiguate'.disambiguate_term ~dbd context metasenv term ~aliases + Disambiguate'.disambiguate_term ~dbd ~context ~metasenv + ?initial_ugraph ~aliases term end end -- 2.39.2