X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Fkernel.ml;fp=matita%2Fcomponents%2Fbinaries%2Fmatex%2Fkernel.ml;h=8b6a81a3e64d110e40eba37072d2e491054e318d;hb=348f1670b30f52db99187b2e92b45348e18ebbbe;hp=17116677cf6efea62c523bc38709c426dcec9604;hpb=d03e9fa5ea709a937148a67fc115d894e5990063;p=helm.git

diff --git a/matita/components/binaries/matex/kernel.ml b/matita/components/binaries/matex/kernel.ml
index 17116677c..8b6a81a3e 100644
--- a/matita/components/binaries/matex/kernel.ml
+++ b/matita/components/binaries/matex/kernel.ml
@@ -116,7 +116,7 @@ let segments_of_uri u =
    let s = S.sub s (i+2) (l-i-2) in
    X.segments_of_string [] (l-i-2) s
 
-let name_of_reference ss = function
+let names_of_reference ss = function
    | C.Constant (_, name, _, _, _), R.Decl      ->
       ss, name
    | C.Constant (_, name, _, _, _), R.Def _     ->
@@ -136,3 +136,10 @@ let name_of_reference ss = function
       (name :: ss), name
    | _                                          ->
       failwith "name_of_reference"
+
+let resolve_reference = function
+   | R.Ref (u, r) ->
+      let ss = segments_of_uri u in
+      let _, _, _, _, obj = E.get_checked_obj G.status u in  
+      let ss, name = names_of_reference ss (obj, r) in
+      X.rev_map_concat X.id "." "type" ss, name