X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaSync.ml;h=55cb4a45c09d45c887e07c26602934283bc61679;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=a77c2476101f5546acf3cb2445bb6e54f6921f04;hpb=aa6153d8e480abfe52b00e1bc6bd48ef84c48988;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index a77c24761..55cb4a45c 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -53,13 +53,10 @@ let alias_diff ~from status =
 let set_proof_aliases status aliases =
  let new_status = { status with aliases = aliases } in
  let diff = alias_diff ~from:status new_status in
- let textual_diff =
-  if DisambiguateTypes.Environment.is_empty diff then
-   ""
-  else
-   DisambiguatePp.pp_environment diff ^ "\n" in
- let moo_content_rev = textual_diff :: status.moo_content_rev in
- {new_status with moo_content_rev = moo_content_rev}
+ if DisambiguateTypes.Environment.is_empty diff then
+   new_status
+ else
+   add_moo_content (DisambiguatePp.commands_of_environment diff) new_status
   
 (** given a uri and a type list (the contructors types) builds a list of pairs
  *  (name,uri) that is used to generate authomatic aliases **)