X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FdisambiguatingParser.ml.in;h=c3302c8b97bb3ddc86c86ba2bfe68279970bff1a;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=dfab60433c75d285dd38e1590071d7303fa68dc9;hpb=d5edcb5c5314fe6cc79bdc5980aa561eaa8e600c;p=helm.git diff --git a/helm/gTopLevel/disambiguatingParser.ml.in b/helm/gTopLevel/disambiguatingParser.ml.in index dfab60433..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 ~(dbh:Dbi.connection) 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 ~dbh context metasenv term ~aliases + Disambiguate'.disambiguate_term ~dbd ~context ~metasenv + ?initial_ugraph ~aliases term end end