- lexiconSync merged into grafiteDisambiguate

[helm.git] / matita / components / grafite_engine / grafiteEngine.ml

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 8d299a533411e71502325418a4e682b8041b8b61..30c176fd2a3cd98188c2aaf8b02955aa4e391c37 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -409,7 +409,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
      let status, composites =
       NCicCoercDeclaration.eval_ncoercion status name t ty source target
      in
-      LexiconSync.add_aliases_for_objs status composites
+      GrafiteDisambiguate.add_aliases_for_objs status composites
   | GrafiteAst.NQed loc ->
      if status#ng_mode <> `ProofMode then
       raise (GrafiteTypes.Command_error "Not in proof mode")
@@ -479,7 +479,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
            let uris = uri::List.rev uris_rev in
 *)
            let status = status#set_ng_mode `CommandMode in
-           let status = LexiconSync.add_aliases_for_objs status [uri] in
+           let status = GrafiteDisambiguate.add_aliases_for_objs status [uri] in
            let status =
             List.fold_left
              (fun status boxml ->
@@ -550,7 +550,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
                       status (name,t,cpos,arity)
                  in
-                  LexiconSync.add_aliases_for_objs status nuris
+                  GrafiteDisambiguate.add_aliases_for_objs status nuris
                with MultiPassDisambiguator.DisambiguationError _-> 
                  HLog.warn ("error in generating coercion: "^name);
                  status)