- lexiconSync merged into grafiteDisambiguate

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

diff --git a/matita/components/lexicon/grafiteDisambiguate.ml b/matita/components/lexicon/grafiteDisambiguate.ml
index 058ddaec3879eca4d4e2e860bb2192af408721c9..88915c893bfec5082860a0201054a38619649555 100644 (file)
--- a/matita/components/lexicon/grafiteDisambiguate.ml
+++ b/matita/components/lexicon/grafiteDisambiguate.ml
@@ -314,3 +314,19 @@ let disambiguate_cic_appl_pattern status args =
  in
   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