X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FdisambiguatingParser.ml.in;h=224eb4b6e913bf4bf58cc262838154a381c2e910;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=25953b50279925c9a28bf18289c6a7ab7aa26917;hpb=1bd503d31db62ec1f4b1dfb416c11615f3af7248;p=helm.git

diff --git a/helm/gTopLevel/disambiguatingParser.ml.in b/helm/gTopLevel/disambiguatingParser.ml.in
index 25953b502..224eb4b6e 100644
--- a/helm/gTopLevel/disambiguatingParser.ml.in
+++ b/helm/gTopLevel/disambiguatingParser.ml.in
@@ -27,23 +27,23 @@ exception NoWellTypedInterpretation
 
 module AndreaAndZackDisambiguatingParser =
  struct
-  module EnvironmentP3 = DisambiguateTypes.EnvironmentP3
+  module EnvironmentP3 = CicTextualParser2.EnvironmentP3
 
   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 term_as_string
+      aliases
     =
-     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 term ~aliases
    end
  end
 
 
+(*
 module CSCTextualDisambiguatingParser =
  struct
   module EnvironmentP3 = OldDisambiguate.EnvironmentP3
@@ -97,6 +97,7 @@ module CSCTexDisambiguatingParser =
           context metasenv dom mk_metasenv_and_expr environment
    end
  end
+*)
 
 @CHOSEN_TERM_PARSER@