Implicit aliases are now defined as all the aliases whose baseuri is the

baseuri of the current development. Much much cleaner.

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 49c3046b8eafeeaf74d0ccaa89635ac1df1289d4..9b9e870855b2b74f2de8656942d1a65dc399f30c 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -126,13 +126,14 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   let initial_space,status,new_status_and_text_list_rev = 
     let module DTE = DisambiguateTypes.Environment in
     let module UM = UriManager in
+    let baseuri = MatitaTypes.get_string_option new_status "baseuri" in
     List.fold_left (
       fun (initial_space,status,acc) (k,((v,_) as value)) -> 
-        let b = 
-          try
-            let v = UM.strip_xpointer (UM.uri_of_string v) in
-            List.mem v new_status.objects 
-          with UM.IllFormedUri _ -> false
+        let b =
+         try
+          UM.buri_of_uri (UM.uri_of_string v) = baseuri
+         with
+          UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
         in
         if b then 
           initial_space,status,acc