X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Falpha.ml;h=b4d4b31cddb281352af8d90278649c6174f21e94;hb=refs%2Fheads%2Fmaster;hp=816edd4a54ab14869b0ddeddc1b696ddd2743744;hpb=d03e9fa5ea709a937148a67fc115d894e5990063;p=helm.git

diff --git a/matita/components/binaries/matex/alpha.ml b/matita/components/binaries/matex/alpha.ml
index 816edd4a5..b4d4b31cd 100644
--- a/matita/components/binaries/matex/alpha.ml
+++ b/matita/components/binaries/matex/alpha.ml
@@ -17,7 +17,6 @@ module H = Hashtbl
 
 module U = NUri
 module C = NCic
-module R = NReference
 module E = NCicEnvironment
 module T = NCicTypeChecker
 
@@ -73,11 +72,9 @@ let get_constant c t = match strip (K.whd c t) with
       P.sprintf "Type[%s]" (U.string_of_uri u)
    | C.Sort (C.Type [`CProp, u]) ->
       P.sprintf "CProp[%s]" (U.string_of_uri u)
-   | C.Const (R.Ref (u, r))      ->
-      let ss = K.segments_of_uri u in
-      let _, _, _, _, obj = E.get_checked_obj G.status u in  
-      let ss, _ = K.name_of_reference ss (obj, r) in
-      X.rev_map_concat X.id "." "type" ss
+   | C.Const c                   ->
+      let s, _ = K.resolve_reference c in
+      s
    | _                           -> ""
 
 let read l s r =
@@ -117,7 +114,7 @@ let global_apha st s =
 try 
    let i = H.find st.g s in
    H.replace st.g s (succ i);
-   P.sprintf "%s.%u" s i
+   P.sprintf "%s_%u" s i
 with Not_found ->
    H.add st.g s 0;
    s
@@ -167,16 +164,16 @@ and proc_terms st ts =
 let proc_named_term s st t =
 try
    let tt = proc_term st t in
-   if !G.test then begin
+   if !G.check then begin
       let _ = K.typeof st.c tt in
       ok s
    end;
    tt
 with
+   | E.ObjectNotFound s 
    | T.TypeCheckerFailure s
    | T.AssertFailure s           -> malformed (Lazy.force s)
 
 (* interface functions ******************************************************)
 
 let process_top_term s t = proc_named_term s (init ()) t
-