A "\n" is now prepended to the aliases that are inserted (to avoid the

creation of horrible long lines).

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 4425d10218521600380b721216d8b98569e636b5..bd0441bc32f9f622629def426d9dece89716336f 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -130,7 +130,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
     if DisambiguateTypes.Environment.is_empty new_aliases then
       parsed_text
     else
-      prepend_text (DisambiguatePp.pp_environment new_aliases)
+      prepend_text ("\n" ^ DisambiguatePp.pp_environment new_aliases)
         parsed_text
   in
   let new_text =