]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/disambiguatingParser.ml.in
ocaml 3.09 transition
[helm.git] / helm / gTopLevel / disambiguatingParser.ml.in
index 6ba3b26ee8bf620afa36bbbb151a84ebdfa290fe..c3302c8b97bb3ddc86c86ba2bfe68279970bff1a 100644 (file)
@@ -31,19 +31,20 @@ module AndreaAndZackDisambiguatingParser =
 
   module Make (C : DisambiguateTypes.Callbacks) =
    struct
-    let
-     disambiguate_term mqi_handle context metasenv term_as_string environment
+    let disambiguate_term ~(dbd:Mysql.dbd) ~context ~metasenv
+      ?initial_ugraph ~aliases term_as_string
     =
-     let module Disambiguate' = Disambiguate.Make (C) in
+      let module Disambiguate' = Disambiguate.Make (C) in
       let term =
-       CicTextualParser2.parse_term (Stream.of_string term_as_string)
+        CicTextualParser2.parse_term (Stream.of_string term_as_string)
       in
-       Disambiguate'.disambiguate_term
-        mqi_handle context metasenv term environment
+      Disambiguate'.disambiguate_term ~dbd ~context ~metasenv
+        ?initial_ugraph ~aliases term
    end
  end
 
 
+(*
 module CSCTextualDisambiguatingParser =
  struct
   module EnvironmentP3 = OldDisambiguate.EnvironmentP3
@@ -97,6 +98,7 @@ module CSCTexDisambiguatingParser =
           context metasenv dom mk_metasenv_and_expr environment
    end
  end
+*)
 
 @CHOSEN_TERM_PARSER@