X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;h=490780fbe2e7adadcc2f3b015ec350231a39f994;hb=2b4ed41c3d8a105f1f9921b37e7f11160001bbe7;hp=88915c893bfec5082860a0201054a38619649555;hpb=791d52ba005e434be27cca1f8059d9f28da0183b;p=helm.git

diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
index 88915c893..490780fbe 100644
--- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -71,11 +71,6 @@ let set_proof_aliases status ~implicit_aliases mode new_aliases =
  if mode = GrafiteAst.WithoutPreferences then
    status
  else
-   (* MATITA 1.0
-   let new_commands =
-     List.map
-      (fun _,alias -> GrafiteAst.Alias (HExtlib.dummy_floc, alias)) new_aliases
-   in *)
    let aliases =
     List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
      status#disambiguate_db.aliases new_aliases in
@@ -315,18 +310,14 @@ let disambiguate_cic_appl_pattern status args =
   disambiguate
 ;;
 
-let add_aliases_for_objs status =
- List.fold_left
-  (fun status nref ->
-    let references = NCicLibrary.aliases_of nref in
-    let new_env =
-     List.map
-      (fun u ->
-        let name = NCicPp.r2s true u in
-         DisambiguateTypes.Id name,
-          GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
-      ) references
-    in
-     set_proof_aliases status ~implicit_aliases:false
-      GrafiteAst.WithPreferences new_env
-  ) status
+let aliases_for_objs refs =
+ List.concat
+  (List.map
+    (fun nref ->
+      let references = NCicLibrary.aliases_of nref in
+       List.map
+        (fun u ->
+          let name = NCicPp.r2s true u in
+           DisambiguateTypes.Id name,
+            GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
+        ) references) refs)