initial support for LaTeX-defined notatopn

[helm.git] / matita / components / binaries / matex / alpha.ml

diff --git a/matita/components/binaries/matex/alpha.ml b/matita/components/binaries/matex/alpha.ml
index 816edd4a54ab14869b0ddeddc1b696ddd2743744..4c4eccef70c0a81fad22842244f41547d10ea80f 100644 (file)
--- a/matita/components/binaries/matex/alpha.ml
+++ b/matita/components/binaries/matex/alpha.ml
@@ -73,11 +73,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 =
@@ -173,6 +171,7 @@ try
    end;
    tt
 with
+   | E.ObjectNotFound s 
    | T.TypeCheckerFailure s
    | T.AssertFailure s           -> malformed (Lazy.force s)