added automathic aliases.

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index c8fbba9bee8a66c777ff205cb0d351aef5841ff4..58043bbd3d5acb44ab3af00adb206135c8f12f24 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -85,6 +85,19 @@ let eval_with_engine status user_goal parsed_text st =
           DisambiguateTypes.Environment.empty
       | _ -> MatitaSync.alias_diff ~from:status new_status
   in
+  (* we remove the defined object since we consider them "automathic aliases" *)
+  let new_aliases = 
+    let module DTE = DisambiguateTypes.Environment in
+    let module UM = UriManager in
+    DTE.fold (
+      fun k ((v,_) as value) acc -> 
+        let v = UM.strip_xpointer (UM.uri_of_string v) in
+        if List.exists (fun (s,_) -> s = v) new_status.objects then
+          acc
+        else
+          DTE.add k value acc
+    ) new_aliases DTE.empty
+  in
   let new_text =
     if DisambiguateTypes.Environment.is_empty new_aliases then
       parsed_text