]> matita.cs.unibo.it Git - helm.git/commitdiff
bugfix: patched .ml.in instaned of .ml :-(
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 27 Apr 2005 17:25:58 +0000 (17:25 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 27 Apr 2005 17:25:58 +0000 (17:25 +0000)
helm/gTopLevel/disambiguatingParser.ml.in

index 224eb4b6e913bf4bf58cc262838154a381c2e910..c3302c8b97bb3ddc86c86ba2bfe68279970bff1a 100644 (file)
@@ -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