Back-porting from new Matita:

[helm.git] / matita / components / ng_disambiguation / grafiteDisambiguate.ml

diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
index 88915c893bfec5082860a0201054a38619649555..490780fbe2e7adadcc2f3b015ec350231a39f994 100644 (file)
--- 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)